diff options
Diffstat (limited to 'theories/theories.itarget')
| -rw-r--r-- | theories/theories.itarget | 401 |
1 files changed, 22 insertions, 379 deletions
diff --git a/theories/theories.itarget b/theories/theories.itarget index 99b059f51..afc3554b1 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -1,379 +1,22 @@ -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 -Arith/NatOrderedType.vo -Arith/MinMax.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 -Classes/RelationPairs.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/FSetCompat.vo -FSets/FSetAVL.vo -FSets/FSetBridge.vo -FSets/FSetDecide.vo -FSets/FSetEqProperties.vo -FSets/FSetFacts.vo -FSets/FSetInterface.vo -FSets/FSetList.vo -FSets/FSetProperties.vo -FSets/FSets.vo -FSets/FSetToFiniteSet.vo -FSets/FSetWeakList.vo - -MSets/MSetAVL.vo -MSets/MSetDecide.vo -MSets/MSetEqProperties.vo -MSets/MSetFacts.vo -MSets/MSetInterface.vo -MSets/MSetList.vo -MSets/MSetProperties.vo -MSets/MSets.vo -MSets/MSetToFiniteSet.vo -MSets/MSetWeakList.vo - -Structures/OrderedTypeAlt.vo -Structures/OrderedTypeEx.vo -Structures/OrderedType.vo -Structures/DecidableType.vo -Structures/DecidableTypeEx.vo -Structures/OrderedType2Alt.vo -Structures/OrderedType2Ex.vo -Structures/OrderedType2.vo -Structures/OrderedType2Facts.vo -Structures/OrderedType2Lists.vo -Structures/DecidableType2.vo -Structures/DecidableType2Ex.vo -Structures/DecidableType2Facts.vo -Structures/OrderTac.vo -Structures/GenericMinMax.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/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/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 -NArith/POrderedType.vo -NArith/Pminmax.vo -NArith/NOrderedType.vo -NArith/Nminmax.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/ZLt.vo -Numbers/Integer/Abstract/ZMulOrder.vo -Numbers/Integer/Abstract/ZMul.vo -Numbers/Integer/Abstract/ZProperties.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/NatInt/NZProperties.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/NOrder.vo -Numbers/Natural/Abstract/NStrongRec.vo -Numbers/Natural/Abstract/NSub.vo -Numbers/Natural/Abstract/NProperties.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/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 -Reals/ROrderedType.vo -Reals/Rminmax.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 -ZArith/ZOrderedType.vo
\ No newline at end of file +Arith/vo.otarget +Bool/vo.otarget +Classes/vo.otarget +FSets/vo.otarget +MSets/vo.otarget +Structures/vo.otarget +Init/vo.otarget +Lists/vo.otarget +Logic/vo.otarget +NArith/vo.otarget +Numbers/vo.otarget +Program/vo.otarget +QArith/vo.otarget +Reals/vo.otarget +Relations/vo.otarget +Setoids/vo.otarget +Sets/vo.otarget +Sorting/vo.otarget +Strings/vo.otarget +Unicode/vo.otarget +Wellfounded/vo.otarget +ZArith/vo.otarget |