@@ -31,7 +31,7 @@ through the <tt>Require Import</tt> command.</p>
31
31
(theories/Init/Prelude.v)
32
32
</dd>
33
33
34
- <dt id="Binary-numbers"> <b >Binary numbers</b>:
34
+ <dt id="Binary-numbers"> <a href="#Binary-numbers" >Binary numbers</b></a >:
35
35
Basic definitions of binary arithmetic
36
36
</dt>
37
37
<dd>
@@ -41,7 +41,7 @@ through the <tt>Require Import</tt> command.</p>
41
41
theories/BinNums/IntDef.v
42
42
</dd>
43
43
44
- <dt id="Cyclic"> <b>Cyclic</b>:
44
+ <dt id="Cyclic"> <a href="#Cyclic">< b>Cyclic</b></a >:
45
45
63-bits-based cyclic arithmetic
46
46
</dt>
47
47
<dd>
@@ -51,7 +51,7 @@ through the <tt>Require Import</tt> command.</p>
51
51
theories/Numbers/Cyclic/Int63/Sint63Axioms.v
52
52
</dd>
53
53
54
- <dt id="Floats"> <b>Floats</b>:
54
+ <dt id="Floats"> <a href="#Floats">< b>Floats</b></a >:
55
55
Floating-point arithmetic
56
56
</dt>
57
57
<dd>
@@ -62,14 +62,14 @@ through the <tt>Require Import</tt> command.</p>
62
62
theories/Floats/FloatAxioms.v
63
63
</dd>
64
64
65
- <dt id="Relations"> <b>Relations</b>:
65
+ <dt id="Relations"> <a href="#Relations">< b>Relations</b></a >:
66
66
Relations (definitions)
67
67
</dt>
68
68
<dd>
69
69
theories/Relations/Relation_Definitions.v
70
70
</dd>
71
71
72
- <dt id="Classes"> <b>Classes</b>:
72
+ <dt id="Classes"> <a href="#Classes">< b>Classes</b></a >:
73
73
</dt>
74
74
<dd>
75
75
theories/Classes/Init.v
@@ -82,20 +82,20 @@ through the <tt>Require Import</tt> command.</p>
82
82
theories/Classes/SetoidTactics.v
83
83
</dd>
84
84
85
- <dt id="Setoids"> <b>Setoids</b>:
85
+ <dt id="Setoids"> <a href="#Setoids">< b>Setoids</b></a >:
86
86
</dt>
87
87
<dd>
88
88
theories/Setoids/Setoid.v
89
89
</dd>
90
90
91
- <dt id="Lists"> <b>Lists</b>:
91
+ <dt id="Lists"> <a href="#Lists">< b>Lists</b></a >:
92
92
Polymorphic lists
93
93
</dt>
94
94
<dd>
95
95
theories/Lists/ListDef.v
96
96
</dd>
97
97
98
- <dt id="Program"> <b>Program</b>:
98
+ <dt id="Program"> <a href="#Program">< b>Program</b></a >:
99
99
Support for dependently-typed programming
100
100
</dt>
101
101
<dd>
@@ -105,7 +105,7 @@ through the <tt>Require Import</tt> command.</p>
105
105
theories/Program/Utils.v
106
106
</dd>
107
107
108
- <dt id="SSReflect"> <b>SSReflect</b>:
108
+ <dt id="SSReflect"> <a href="#SSReflect">< b>SSReflect</b></a >:
109
109
Base libraries for the SSReflect proof language and the
110
110
small scale reflection formalization technique
111
111
</dt>
@@ -117,7 +117,7 @@ through the <tt>Require Import</tt> command.</p>
117
117
theories/ssr/ssrfun.v
118
118
</dd>
119
119
120
- <dt id="Ltac2"> <b>Ltac2</b>:
120
+ <dt id="Ltac2"> <a href="#Ltac2">< b>Ltac2</b></a >:
121
121
The Ltac2 tactic programming language
122
122
</dt>
123
123
<dd>
@@ -159,7 +159,7 @@ through the <tt>Require Import</tt> command.</p>
159
159
user-contrib/Ltac2/Unification.v
160
160
</dd>
161
161
162
- <dt id="Compat"> <b>Compat</b>:
162
+ <dt id="Compat"> <a href="#Compat">< b>Compat</b></a >:
163
163
Compatibility wrappers for previous versions of Coq
164
164
</dt>
165
165
<dd>
@@ -171,15 +171,15 @@ through the <tt>Require Import</tt> command.</p>
171
171
user-contrib/Ltac2/Compat/Coq819.v
172
172
</dd>
173
173
174
- <dt id="Array"> <b>Array</b>:
174
+ <dt id="Array"> <a href="#Array">< b>Array</b></a >:
175
175
Persistent native arrays
176
176
</dt>
177
177
<dd>
178
178
theories/Array/PrimArray.v
179
179
theories/Array/ArrayAxioms.v
180
180
</dd>
181
181
182
- <dt id="Primitive-strings> <b>Primitive strings</b>:
182
+ <dt id="Primitive-strings" > <a href="#Primitive-strings">< b>Primitive strings</b></a >:
183
183
Native string type
184
184
</dt>
185
185
<dd>
0 commit comments