aboutsummaryrefslogtreecommitdiffhomepage
path: root/vo.itarget
blob: 8898dd8fa0fb6eedc56ed4455569a3d381b631d2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
theories/Arith/Arith_base.vo
theories/Arith/Arith.vo
theories/Arith/Between.vo
theories/Arith/Bool_nat.vo
theories/Arith/Compare_dec.vo
theories/Arith/Compare.vo
theories/Arith/Div2.vo
theories/Arith/EqNat.vo
theories/Arith/Euclid.vo
theories/Arith/Even.vo
theories/Arith/Factorial.vo
theories/Arith/Gt.vo
theories/Arith/Le.vo
theories/Arith/Lt.vo
theories/Arith/Max.vo
theories/Arith/Minus.vo
theories/Arith/Min.vo
theories/Arith/Mult.vo
theories/Arith/Peano_dec.vo
theories/Arith/Plus.vo
theories/Arith/Wf_nat.vo

theories/Bool/BoolEq.vo
theories/Bool/Bool.vo
theories/Bool/Bvector.vo
theories/Bool/DecBool.vo
theories/Bool/IfProp.vo
theories/Bool/Sumbool.vo
theories/Bool/Zerob.vo

theories/Classes/Equivalence.vo
theories/Classes/EquivDec.vo
theories/Classes/Functions.vo
theories/Classes/Init.vo
theories/Classes/Morphisms_Prop.vo
theories/Classes/Morphisms_Relations.vo
theories/Classes/Morphisms.vo
theories/Classes/RelationClasses.vo
theories/Classes/SetoidAxioms.vo
theories/Classes/SetoidClass.vo
theories/Classes/SetoidDec.vo
theories/Classes/SetoidTactics.vo

theories/FSets/FMapAVL.vo
theories/FSets/FMapFacts.vo
theories/FSets/FMapFullAVL.vo
theories/FSets/FMapInterface.vo
theories/FSets/FMapList.vo
theories/FSets/FMapPositive.vo
theories/FSets/FMaps.vo
theories/FSets/FMapWeakList.vo
theories/FSets/FSetAVL.vo
theories/FSets/FSetBridge.vo
theories/FSets/FSetDecide.vo
theories/FSets/FSetEqProperties.vo
theories/FSets/FSetFacts.vo
theories/FSets/FSetFullAVL.vo
theories/FSets/FSetInterface.vo
theories/FSets/FSetList.vo
theories/FSets/FSetProperties.vo
theories/FSets/FSets.vo
theories/FSets/FSetToFiniteSet.vo
theories/FSets/FSetWeakList.vo
theories/FSets/OrderedTypeAlt.vo
theories/FSets/OrderedTypeEx.vo
theories/FSets/OrderedType.vo

theories/Init/Datatypes.vo
theories/Init/Logic_Type.vo
theories/Init/Logic.vo
theories/Init/Notations.vo
theories/Init/Peano.vo
theories/Init/Prelude.vo
theories/Init/Specif.vo
theories/Init/Tactics.vo
theories/Init/Wf.vo

theories/Lists/ListSet.vo
theories/Lists/ListTactics.vo
theories/Lists/List.vo
theories/Lists/MonoList.vo
theories/Lists/SetoidList.vo
theories/Lists/StreamMemo.vo
theories/Lists/Streams.vo
theories/Lists/TheoryList.vo

theories/Logic/Berardi.vo
theories/Logic/ChoiceFacts.vo
theories/Logic/ClassicalChoice.vo
theories/Logic/ClassicalDescription.vo
theories/Logic/ClassicalEpsilon.vo
theories/Logic/ClassicalFacts.vo
theories/Logic/Classical_Pred_Set.vo
theories/Logic/Classical_Pred_Type.vo
theories/Logic/Classical_Prop.vo
theories/Logic/Classical_Type.vo
theories/Logic/ClassicalUniqueChoice.vo
theories/Logic/Classical.vo
theories/Logic/ConstructiveEpsilon.vo
theories/Logic/DecidableTypeEx.vo
theories/Logic/DecidableType.vo
theories/Logic/Decidable.vo
theories/Logic/Description.vo
theories/Logic/Diaconescu.vo
theories/Logic/Epsilon.vo
theories/Logic/Eqdep_dec.vo
theories/Logic/EqdepFacts.vo
theories/Logic/Eqdep.vo
theories/Logic/FunctionalExtensionality.vo
theories/Logic/Hurkens.vo
theories/Logic/IndefiniteDescription.vo
theories/Logic/JMeq.vo
theories/Logic/ProofIrrelevanceFacts.vo
theories/Logic/ProofIrrelevance.vo
theories/Logic/RelationalChoice.vo
theories/Logic/SetIsType.vo

theories/NArith/BinNat.vo
theories/NArith/BinPos.vo
theories/NArith/NArith.vo
theories/NArith/Ndec.vo
theories/NArith/Ndigits.vo
theories/NArith/Ndist.vo
theories/NArith/Nnat.vo
theories/NArith/Pnat.vo

theories/Numbers/BigNumPrelude.vo
theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
theories/Numbers/Cyclic/Abstract/NZCyclic.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
theories/Numbers/Cyclic/Int31/Cyclic31.vo
theories/Numbers/Cyclic/Int31/Int31.vo
theories/Numbers/Cyclic/ZModulo/ZModulo.vo
theories/Numbers/Integer/Abstract/ZAddOrder.vo
theories/Numbers/Integer/Abstract/ZAdd.vo
theories/Numbers/Integer/Abstract/ZAxioms.vo
theories/Numbers/Integer/Abstract/ZBase.vo
#theories/Numbers/Integer/Abstract/ZDomain.vo
theories/Numbers/Integer/Abstract/ZLt.vo
theories/Numbers/Integer/Abstract/ZMulOrder.vo
theories/Numbers/Integer/Abstract/ZMul.vo
theories/Numbers/Integer/BigZ/BigZ.vo
theories/Numbers/Integer/BigZ/ZMake.vo
theories/Numbers/Integer/Binary/ZBinary.vo
theories/Numbers/Integer/NatPairs/ZNatPairs.vo
theories/Numbers/Integer/SpecViaZ/ZSig.vo
theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo
theories/Numbers/NaryFunctions.vo
theories/Numbers/NatInt/NZAddOrder.vo
theories/Numbers/NatInt/NZAdd.vo
theories/Numbers/NatInt/NZAxioms.vo
theories/Numbers/NatInt/NZBase.vo
theories/Numbers/NatInt/NZMulOrder.vo
theories/Numbers/NatInt/NZMul.vo
theories/Numbers/NatInt/NZOrder.vo
theories/Numbers/Natural/Abstract/NAddOrder.vo
theories/Numbers/Natural/Abstract/NAdd.vo
theories/Numbers/Natural/Abstract/NAxioms.vo
theories/Numbers/Natural/Abstract/NBase.vo
#theories/Numbers/Natural/Abstract/NDefOps.vo
theories/Numbers/Natural/Abstract/NIso.vo
theories/Numbers/Natural/Abstract/NMulOrder.vo
theories/Numbers/Natural/Abstract/NMul.vo
theories/Numbers/Natural/Abstract/NOrder.vo
#theories/Numbers/Natural/Abstract/NStrongRec.vo
theories/Numbers/Natural/Abstract/NSub.vo
theories/Numbers/Natural/BigN/BigN.vo
theories/Numbers/Natural/BigN/Nbasic.vo
theories/Numbers/Natural/Binary/NBinary.vo
theories/Numbers/Natural/Binary/NBinDefs.vo
theories/Numbers/Natural/Peano/NPeano.vo
theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo
theories/Numbers/Natural/SpecViaZ/NSig.vo
theories/Numbers/NumPrelude.vo
theories/Numbers/Rational/BigQ/BigQ.vo
theories/Numbers/Rational/BigQ/QMake.vo
theories/Numbers/Rational/SpecViaQ/QSig.vo

theories/Program/Basics.vo
theories/Program/Combinators.vo
theories/Program/Equality.vo
theories/Program/Program.vo
theories/Program/Subset.vo
theories/Program/Syntax.vo
theories/Program/Tactics.vo
theories/Program/Utils.vo
theories/Program/Wf.vo

theories/QArith/Qabs.vo
theories/QArith/QArith_base.vo
theories/QArith/QArith.vo
theories/QArith/Qcanon.vo
theories/QArith/Qfield.vo
theories/QArith/Qpower.vo
theories/QArith/Qreals.vo
theories/QArith/Qreduction.vo
theories/QArith/Qring.vo
theories/QArith/Qround.vo

theories/Reals/Alembert.vo
theories/Reals/AltSeries.vo
theories/Reals/ArithProp.vo
theories/Reals/Binomial.vo
theories/Reals/Cauchy_prod.vo
theories/Reals/Cos_plus.vo
theories/Reals/Cos_rel.vo
theories/Reals/DiscrR.vo
theories/Reals/Exp_prop.vo
theories/Reals/Integration.vo
theories/Reals/LegacyRfield.vo
theories/Reals/MVT.vo
theories/Reals/NewtonInt.vo
theories/Reals/PartSum.vo
theories/Reals/PSeries_reg.vo
theories/Reals/Ranalysis1.vo
theories/Reals/Ranalysis2.vo
theories/Reals/Ranalysis3.vo
theories/Reals/Ranalysis4.vo
theories/Reals/Ranalysis.vo
theories/Reals/Raxioms.vo
theories/Reals/Rbase.vo
theories/Reals/Rbasic_fun.vo
theories/Reals/Rcomplete.vo
theories/Reals/Rdefinitions.vo
theories/Reals/Rderiv.vo
theories/Reals/Reals.vo
theories/Reals/Rfunctions.vo
theories/Reals/Rgeom.vo
theories/Reals/RiemannInt_SF.vo
theories/Reals/RiemannInt.vo
theories/Reals/R_Ifp.vo
theories/Reals/RIneq.vo
theories/Reals/Rlimit.vo
theories/Reals/RList.vo
theories/Reals/Rlogic.vo
theories/Reals/Rpow_def.vo
theories/Reals/Rpower.vo
theories/Reals/Rprod.vo
theories/Reals/Rseries.vo
theories/Reals/Rsigma.vo
theories/Reals/Rsqrt_def.vo
theories/Reals/R_sqrt.vo
theories/Reals/R_sqr.vo
theories/Reals/Rtopology.vo
theories/Reals/Rtrigo_alt.vo
theories/Reals/Rtrigo_calc.vo
theories/Reals/Rtrigo_def.vo
theories/Reals/Rtrigo_fun.vo
theories/Reals/Rtrigo_reg.vo
theories/Reals/Rtrigo.vo
theories/Reals/SeqProp.vo
theories/Reals/SeqSeries.vo
theories/Reals/SplitAbsolu.vo
theories/Reals/SplitRmult.vo
theories/Reals/Sqrt_reg.vo

theories/Relations/Operators_Properties.vo
theories/Relations/Relation_Definitions.vo
theories/Relations/Relation_Operators.vo
theories/Relations/Relations.vo

theories/Setoids/Setoid.vo
theories/Sets/Classical_sets.vo
theories/Sets/Constructive_sets.vo
theories/Sets/Cpo.vo
theories/Sets/Ensembles.vo
theories/Sets/Finite_sets_facts.vo
theories/Sets/Finite_sets.vo
theories/Sets/Image.vo
theories/Sets/Infinite_sets.vo
theories/Sets/Integers.vo
theories/Sets/Multiset.vo
theories/Sets/Partial_Order.vo
theories/Sets/Permut.vo
theories/Sets/Powerset_Classical_facts.vo
theories/Sets/Powerset_facts.vo
theories/Sets/Powerset.vo
theories/Sets/Relations_1_facts.vo
theories/Sets/Relations_1.vo
theories/Sets/Relations_2_facts.vo
theories/Sets/Relations_2.vo
theories/Sets/Relations_3_facts.vo
theories/Sets/Relations_3.vo
theories/Sets/Uniset.vo

theories/Sorting/Heap.vo
theories/Sorting/Permutation.vo
theories/Sorting/PermutEq.vo
theories/Sorting/PermutSetoid.vo
theories/Sorting/Sorting.vo

theories/Strings/Ascii.vo
theories/Strings/String.vo

theories/Unicode/Utf8.vo

theories/Wellfounded/Disjoint_Union.vo
theories/Wellfounded/Inclusion.vo
theories/Wellfounded/Inverse_Image.vo
theories/Wellfounded/Lexicographic_Exponentiation.vo
theories/Wellfounded/Lexicographic_Product.vo
theories/Wellfounded/Transitive_Closure.vo
theories/Wellfounded/Union.vo
theories/Wellfounded/Wellfounded.vo
theories/Wellfounded/Well_Ordering.vo

theories/ZArith/auxiliary.vo
theories/ZArith/BinInt.vo
theories/ZArith/Int.vo
theories/ZArith/Wf_Z.vo
theories/ZArith/Zabs.vo
theories/ZArith/ZArith_base.vo
theories/ZArith/ZArith_dec.vo
theories/ZArith/ZArith.vo
theories/ZArith/Zbinary.vo
theories/ZArith/Zbool.vo
theories/ZArith/Zcompare.vo
theories/ZArith/Zcomplements.vo
theories/ZArith/Zdiv.vo
theories/ZArith/Zeven.vo
theories/ZArith/Zgcd_alt.vo
theories/ZArith/Zhints.vo
theories/ZArith/Zlogarithm.vo
theories/ZArith/Zmax.vo
theories/ZArith/Zminmax.vo
theories/ZArith/Zmin.vo
theories/ZArith/Zmisc.vo
theories/ZArith/Znat.vo
theories/ZArith/Znumtheory.vo
theories/ZArith/ZOdiv_def.vo
theories/ZArith/ZOdiv.vo
theories/ZArith/Zorder.vo
theories/ZArith/Zpow_def.vo
theories/ZArith/Zpower.vo
theories/ZArith/Zpow_facts.vo
theories/ZArith/Zsqrt.vo
theories/ZArith/Zwf.vo

plugins/dp/Dp.vo
plugins/field/LegacyField_Compl.vo
plugins/field/LegacyField_Tactic.vo
plugins/field/LegacyField_Theory.vo
plugins/field/LegacyField.vo
plugins/fourier/Fourier_util.vo
plugins/fourier/Fourier.vo
plugins/funind/Recdef.vo
plugins/groebner/GroebnerR.vo
plugins/groebner/GroebnerZ.vo
plugins/interface/CoqInterface.vo
#plugins/interface/CoqParser.vo  (should not be compiled)
plugins/micromega/CheckerMaker.vo
plugins/micromega/EnvRing.vo
plugins/micromega/Env.vo
#plugins/micromega/MExtraction.vo  (extraction of micromega.ml)
plugins/micromega/OrderedRing.vo
plugins/micromega/Psatz.vo
plugins/micromega/QMicromega.vo
plugins/micromega/Refl.vo
plugins/micromega/RingMicromega.vo
plugins/micromega/RMicromega.vo
plugins/micromega/Tauto.vo
plugins/micromega/VarMap.vo
plugins/micromega/ZCoeff.vo
plugins/micromega/ZMicromega.vo
plugins/omega/OmegaLemmas.vo
plugins/omega/OmegaPlugin.vo
plugins/omega/Omega.vo
plugins/omega/PreOmega.vo
plugins/quote/Quote.vo
plugins/ring/LegacyArithRing.vo
plugins/ring/LegacyNArithRing.vo
plugins/ring/LegacyRing_theory.vo
plugins/ring/LegacyRing.vo
plugins/ring/LegacyZArithRing.vo
plugins/ring/Ring_abstract.vo
plugins/ring/Ring_normalize.vo
plugins/ring/Setoid_ring_normalize.vo
plugins/ring/Setoid_ring_theory.vo
plugins/ring/Setoid_ring.vo
plugins/romega/ReflOmegaCore.vo
plugins/romega/ROmega.vo
plugins/rtauto/Bintree.vo
plugins/rtauto/Rtauto.vo
plugins/setoid_ring/ArithRing.vo
plugins/setoid_ring/BinList.vo
plugins/setoid_ring/Field_tac.vo
plugins/setoid_ring/Field_theory.vo
plugins/setoid_ring/Field.vo
plugins/setoid_ring/InitialRing.vo
plugins/setoid_ring/NArithRing.vo
plugins/setoid_ring/RealField.vo
plugins/setoid_ring/Ring_base.vo
plugins/setoid_ring/Ring_equiv.vo
plugins/setoid_ring/Ring_polynom.vo
plugins/setoid_ring/Ring_tac.vo
plugins/setoid_ring/Ring_theory.vo
plugins/setoid_ring/Ring.vo
plugins/setoid_ring/ZArithRing.vo