diff options
Diffstat (limited to 'theories/theories.itarget')
| -rw-r--r-- | theories/theories.itarget | 348 |
1 files changed, 348 insertions, 0 deletions
diff --git a/theories/theories.itarget b/theories/theories.itarget new file mode 100644 index 000000000..7798ebebc --- /dev/null +++ b/theories/theories.itarget @@ -0,0 +1,348 @@ +Arith/Arith_base.vo +Arith/Arith.vo +Arith/Between.vo +Arith/Bool_nat.vo +Arith/Compare_dec.vo +Arith/Compare.vo +Arith/Div2.vo +Arith/EqNat.vo +Arith/Euclid.vo +Arith/Even.vo +Arith/Factorial.vo +Arith/Gt.vo +Arith/Le.vo +Arith/Lt.vo +Arith/Max.vo +Arith/Minus.vo +Arith/Min.vo +Arith/Mult.vo +Arith/Peano_dec.vo +Arith/Plus.vo +Arith/Wf_nat.vo + +Bool/BoolEq.vo +Bool/Bool.vo +Bool/Bvector.vo +Bool/DecBool.vo +Bool/IfProp.vo +Bool/Sumbool.vo +Bool/Zerob.vo + +Classes/Equivalence.vo +Classes/EquivDec.vo +Classes/Functions.vo +Classes/Init.vo +Classes/Morphisms_Prop.vo +Classes/Morphisms_Relations.vo +Classes/Morphisms.vo +Classes/RelationClasses.vo +Classes/SetoidAxioms.vo +Classes/SetoidClass.vo +Classes/SetoidDec.vo +Classes/SetoidTactics.vo + +FSets/FMapAVL.vo +FSets/FMapFacts.vo +FSets/FMapFullAVL.vo +FSets/FMapInterface.vo +FSets/FMapList.vo +FSets/FMapPositive.vo +FSets/FMaps.vo +FSets/FMapWeakList.vo +FSets/FSetAVL.vo +FSets/FSetBridge.vo +FSets/FSetDecide.vo +FSets/FSetEqProperties.vo +FSets/FSetFacts.vo +FSets/FSetFullAVL.vo +FSets/FSetInterface.vo +FSets/FSetList.vo +FSets/FSetProperties.vo +FSets/FSets.vo +FSets/FSetToFiniteSet.vo +FSets/FSetWeakList.vo +FSets/OrderedTypeAlt.vo +FSets/OrderedTypeEx.vo +FSets/OrderedType.vo + +Init/Datatypes.vo +Init/Logic_Type.vo +Init/Logic.vo +Init/Notations.vo +Init/Peano.vo +Init/Prelude.vo +Init/Specif.vo +Init/Tactics.vo +Init/Wf.vo + +Lists/ListSet.vo +Lists/ListTactics.vo +Lists/List.vo +Lists/MonoList.vo +Lists/SetoidList.vo +Lists/StreamMemo.vo +Lists/Streams.vo +Lists/TheoryList.vo + +Logic/Berardi.vo +Logic/ChoiceFacts.vo +Logic/ClassicalChoice.vo +Logic/ClassicalDescription.vo +Logic/ClassicalEpsilon.vo +Logic/ClassicalFacts.vo +Logic/Classical_Pred_Set.vo +Logic/Classical_Pred_Type.vo +Logic/Classical_Prop.vo +Logic/Classical_Type.vo +Logic/ClassicalUniqueChoice.vo +Logic/Classical.vo +Logic/ConstructiveEpsilon.vo +Logic/DecidableTypeEx.vo +Logic/DecidableType.vo +Logic/Decidable.vo +Logic/Description.vo +Logic/Diaconescu.vo +Logic/Epsilon.vo +Logic/Eqdep_dec.vo +Logic/EqdepFacts.vo +Logic/Eqdep.vo +Logic/FunctionalExtensionality.vo +Logic/Hurkens.vo +Logic/IndefiniteDescription.vo +Logic/JMeq.vo +Logic/ProofIrrelevanceFacts.vo +Logic/ProofIrrelevance.vo +Logic/RelationalChoice.vo +Logic/SetIsType.vo + +NArith/BinNat.vo +NArith/BinPos.vo +NArith/NArith.vo +NArith/Ndec.vo +NArith/Ndigits.vo +NArith/Ndist.vo +NArith/Nnat.vo +NArith/Pnat.vo + +Numbers/BigNumPrelude.vo +Numbers/Cyclic/Abstract/CyclicAxioms.vo +Numbers/Cyclic/Abstract/NZCyclic.vo +Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo +Numbers/Cyclic/DoubleCyclic/DoubleBase.vo +Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo +Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo +Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo +Numbers/Cyclic/DoubleCyclic/DoubleLift.vo +Numbers/Cyclic/DoubleCyclic/DoubleMul.vo +Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo +Numbers/Cyclic/DoubleCyclic/DoubleSub.vo +Numbers/Cyclic/DoubleCyclic/DoubleType.vo +Numbers/Cyclic/Int31/Cyclic31.vo +Numbers/Cyclic/Int31/Int31.vo +Numbers/Cyclic/ZModulo/ZModulo.vo +Numbers/Integer/Abstract/ZAddOrder.vo +Numbers/Integer/Abstract/ZAdd.vo +Numbers/Integer/Abstract/ZAxioms.vo +Numbers/Integer/Abstract/ZBase.vo +#Numbers/Integer/Abstract/ZDomain.vo +Numbers/Integer/Abstract/ZLt.vo +Numbers/Integer/Abstract/ZMulOrder.vo +Numbers/Integer/Abstract/ZMul.vo +Numbers/Integer/BigZ/BigZ.vo +Numbers/Integer/BigZ/ZMake.vo +Numbers/Integer/Binary/ZBinary.vo +Numbers/Integer/NatPairs/ZNatPairs.vo +Numbers/Integer/SpecViaZ/ZSig.vo +Numbers/Integer/SpecViaZ/ZSigZAxioms.vo +Numbers/NaryFunctions.vo +Numbers/NatInt/NZAddOrder.vo +Numbers/NatInt/NZAdd.vo +Numbers/NatInt/NZAxioms.vo +Numbers/NatInt/NZBase.vo +Numbers/NatInt/NZMulOrder.vo +Numbers/NatInt/NZMul.vo +Numbers/NatInt/NZOrder.vo +Numbers/Natural/Abstract/NAddOrder.vo +Numbers/Natural/Abstract/NAdd.vo +Numbers/Natural/Abstract/NAxioms.vo +Numbers/Natural/Abstract/NBase.vo +#Numbers/Natural/Abstract/NDefOps.vo +Numbers/Natural/Abstract/NIso.vo +Numbers/Natural/Abstract/NMulOrder.vo +Numbers/Natural/Abstract/NMul.vo +Numbers/Natural/Abstract/NOrder.vo +#Numbers/Natural/Abstract/NStrongRec.vo +Numbers/Natural/Abstract/NSub.vo +Numbers/Natural/BigN/BigN.vo +Numbers/Natural/BigN/Nbasic.vo +# Beware: source file for the next one is generated by a script +Numbers/Natural/BigN/NMake.vo +Numbers/Natural/Binary/NBinary.vo +Numbers/Natural/Binary/NBinDefs.vo +Numbers/Natural/Peano/NPeano.vo +Numbers/Natural/SpecViaZ/NSigNAxioms.vo +Numbers/Natural/SpecViaZ/NSig.vo +Numbers/NumPrelude.vo +Numbers/Rational/BigQ/BigQ.vo +Numbers/Rational/BigQ/QMake.vo +Numbers/Rational/SpecViaQ/QSig.vo + +Program/Basics.vo +Program/Combinators.vo +Program/Equality.vo +Program/Program.vo +Program/Subset.vo +Program/Syntax.vo +Program/Tactics.vo +Program/Utils.vo +Program/Wf.vo + +QArith/Qabs.vo +QArith/QArith_base.vo +QArith/QArith.vo +QArith/Qcanon.vo +QArith/Qfield.vo +QArith/Qpower.vo +QArith/Qreals.vo +QArith/Qreduction.vo +QArith/Qring.vo +QArith/Qround.vo + +Reals/Alembert.vo +Reals/AltSeries.vo +Reals/ArithProp.vo +Reals/Binomial.vo +Reals/Cauchy_prod.vo +Reals/Cos_plus.vo +Reals/Cos_rel.vo +Reals/DiscrR.vo +Reals/Exp_prop.vo +Reals/Integration.vo +Reals/LegacyRfield.vo +Reals/MVT.vo +Reals/NewtonInt.vo +Reals/PartSum.vo +Reals/PSeries_reg.vo +Reals/Ranalysis1.vo +Reals/Ranalysis2.vo +Reals/Ranalysis3.vo +Reals/Ranalysis4.vo +Reals/Ranalysis.vo +Reals/Raxioms.vo +Reals/Rbase.vo +Reals/Rbasic_fun.vo +Reals/Rcomplete.vo +Reals/Rdefinitions.vo +Reals/Rderiv.vo +Reals/Reals.vo +Reals/Rfunctions.vo +Reals/Rgeom.vo +Reals/RiemannInt_SF.vo +Reals/RiemannInt.vo +Reals/R_Ifp.vo +Reals/RIneq.vo +Reals/Rlimit.vo +Reals/RList.vo +Reals/Rlogic.vo +Reals/Rpow_def.vo +Reals/Rpower.vo +Reals/Rprod.vo +Reals/Rseries.vo +Reals/Rsigma.vo +Reals/Rsqrt_def.vo +Reals/R_sqrt.vo +Reals/R_sqr.vo +Reals/Rtopology.vo +Reals/Rtrigo_alt.vo +Reals/Rtrigo_calc.vo +Reals/Rtrigo_def.vo +Reals/Rtrigo_fun.vo +Reals/Rtrigo_reg.vo +Reals/Rtrigo.vo +Reals/SeqProp.vo +Reals/SeqSeries.vo +Reals/SplitAbsolu.vo +Reals/SplitRmult.vo +Reals/Sqrt_reg.vo + +Relations/Operators_Properties.vo +Relations/Relation_Definitions.vo +Relations/Relation_Operators.vo +Relations/Relations.vo + +Setoids/Setoid.vo +Sets/Classical_sets.vo +Sets/Constructive_sets.vo +Sets/Cpo.vo +Sets/Ensembles.vo +Sets/Finite_sets_facts.vo +Sets/Finite_sets.vo +Sets/Image.vo +Sets/Infinite_sets.vo +Sets/Integers.vo +Sets/Multiset.vo +Sets/Partial_Order.vo +Sets/Permut.vo +Sets/Powerset_Classical_facts.vo +Sets/Powerset_facts.vo +Sets/Powerset.vo +Sets/Relations_1_facts.vo +Sets/Relations_1.vo +Sets/Relations_2_facts.vo +Sets/Relations_2.vo +Sets/Relations_3_facts.vo +Sets/Relations_3.vo +Sets/Uniset.vo + +Sorting/Heap.vo +Sorting/Permutation.vo +Sorting/PermutEq.vo +Sorting/PermutSetoid.vo +Sorting/Sorting.vo + +Strings/Ascii.vo +Strings/String.vo + +Unicode/Utf8.vo + +Wellfounded/Disjoint_Union.vo +Wellfounded/Inclusion.vo +Wellfounded/Inverse_Image.vo +Wellfounded/Lexicographic_Exponentiation.vo +Wellfounded/Lexicographic_Product.vo +Wellfounded/Transitive_Closure.vo +Wellfounded/Union.vo +Wellfounded/Wellfounded.vo +Wellfounded/Well_Ordering.vo + +ZArith/auxiliary.vo +ZArith/BinInt.vo +ZArith/Int.vo +ZArith/Wf_Z.vo +ZArith/Zabs.vo +ZArith/ZArith_base.vo +ZArith/ZArith_dec.vo +ZArith/ZArith.vo +ZArith/Zbinary.vo +ZArith/Zbool.vo +ZArith/Zcompare.vo +ZArith/Zcomplements.vo +ZArith/Zdiv.vo +ZArith/Zeven.vo +ZArith/Zgcd_alt.vo +ZArith/Zhints.vo +ZArith/Zlogarithm.vo +ZArith/Zmax.vo +ZArith/Zminmax.vo +ZArith/Zmin.vo +ZArith/Zmisc.vo +ZArith/Znat.vo +ZArith/Znumtheory.vo +ZArith/ZOdiv_def.vo +ZArith/ZOdiv.vo +ZArith/Zorder.vo +ZArith/Zpow_def.vo +ZArith/Zpower.vo +ZArith/Zpow_facts.vo +ZArith/Zsqrt.vo +ZArith/Zwf.vo |