diff options
41 files changed, 507 insertions, 785 deletions
diff --git a/Makefile.build b/Makefile.build index 221fa56a7..4b9dd34f4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -387,18 +387,11 @@ lists: $(LISTSVO) strings: $(STRINGSVO) sets: $(SETSVO) fsets: $(FSETSVO) -allfsets: $(ALLFSETS) relations: $(RELATIONSVO) wellfounded: $(WELLFOUNDEDVO) -# reals reals: $(REALSVO) -allreals: $(ALLREALS) setoids: $(SETOIDSVO) sorting: $(SORTINGVO) -# numbers -natural: $(NATURALVO) -integer: $(INTEGERVO) -rational: $(RATIONALVO) numbers: $(NUMBERSVO) noreal: logic arith bool zarith qarith lists sets fsets relations \ @@ -596,9 +589,6 @@ install-library-light: $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states -$(INSTALLLIB) revision $(FULLCOQLIB) -install-allreals:: - $(INSTALLSH) $(FULLCOQLIB) $(ALLREALS) - install-coq-info: install-coq-manpages install-emacs install-latex install-coq-manpages: diff --git a/Makefile.common b/Makefile.common index 989ce3c58..c04480ef1 100644 --- a/Makefile.common +++ b/Makefile.common @@ -272,238 +272,34 @@ STAGE1:=parsing/grammar.cma parsing/q_constr.cmo # vo files ########################################################################### -## Theories - -INITVO:=$(addprefix theories/Init/, \ - Notations.vo Datatypes.vo Peano.vo Logic.vo \ - Specif.vo Logic_Type.vo Wf.vo Tactics.vo \ - Prelude.vo ) - -LOGICVO:=$(addprefix theories/Logic/, \ - Hurkens.vo ProofIrrelevance.vo Classical.vo \ - Classical_Type.vo Classical_Pred_Set.vo Eqdep.vo \ - Classical_Prop.vo Classical_Pred_Type.vo ClassicalFacts.vo \ - ChoiceFacts.vo Berardi.vo Eqdep_dec.vo \ - Decidable.vo JMeq.vo ClassicalChoice.vo \ - ClassicalDescription.vo RelationalChoice.vo Diaconescu.vo \ - EqdepFacts.vo ProofIrrelevanceFacts.vo ClassicalEpsilon.vo \ - ClassicalUniqueChoice.vo \ - Epsilon.vo ConstructiveEpsilon.vo Description.vo \ - IndefiniteDescription.vo SetIsType.vo FunctionalExtensionality.vo ) - -STRUCTURESVO:=$(addprefix theories/Structures/, \ - OrderTac.vo \ - DecidableType.vo DecidableTypeEx.vo \ - OrderedType.vo OrderedTypeEx.vo OrderedTypeAlt.vo \ - DecidableType2.vo DecidableType2Ex.vo DecidableType2Facts.vo \ - OrderedType2.vo OrderedType2Ex.vo OrderedType2Alt.vo \ - OrderedType2Facts.vo OrderedType2Lists.vo GenericMinMax.vo ) - -ARITHVO:=$(addprefix theories/Arith/, \ - Arith.vo Gt.vo Between.vo Le.vo \ - Compare.vo Lt.vo Compare_dec.vo Min.vo \ - Div2.vo Minus.vo Mult.vo Even.vo \ - EqNat.vo Peano_dec.vo Euclid.vo Plus.vo \ - Wf_nat.vo Max.vo Bool_nat.vo Factorial.vo \ - Arith_base.vo MinMax.vo NatOrderedType.vo ) - -SORTINGVO:=$(addprefix theories/Sorting/, \ - Heap.vo Permutation.vo Sorting.vo PermutSetoid.vo \ - PermutEq.vo ) - -BOOLVO:=$(addprefix theories/Bool/, \ - Bool.vo IfProp.vo Zerob.vo DecBool.vo \ - Sumbool.vo BoolEq.vo Bvector.vo ) - -NARITHVO:=$(addprefix theories/NArith/, \ - BinPos.vo Pnat.vo BinNat.vo NArith.vo \ - Nnat.vo Ndigits.vo Ndec.vo Ndist.vo \ - POrderedType.vo Pminmax.vo NOrderedType.vo Nminmax.vo ) - -ZARITHVO:=$(addprefix theories/ZArith/, \ - BinInt.vo Wf_Z.vo ZArith.vo ZArith_dec.vo \ - auxiliary.vo Zmisc.vo Zcompare.vo Znat.vo \ - Zorder.vo Zabs.vo Zmin.vo Zmax.vo \ - Zminmax.vo Zeven.vo Zhints.vo Zlogarithm.vo \ - Zpower.vo Zcomplements.vo Zdiv.vo Zsqrt.vo \ - Zwf.vo ZArith_base.vo Zbool.vo Zbinary.vo \ - Znumtheory.vo Int.vo Zpow_def.vo Zpow_facts.vo \ - ZOdiv_def.vo ZOdiv.vo Zgcd_alt.vo ZOrderedType.vo ) - -QARITHVO:=$(addprefix theories/QArith/, \ - QArith_base.vo Qreduction.vo Qring.vo Qreals.vo \ - QArith.vo Qcanon.vo Qfield.vo Qpower.vo \ - Qabs.vo Qround.vo ) - -LISTSVO:=$(addprefix theories/Lists/, \ - ListSet.vo Streams.vo StreamMemo.vo \ - TheoryList.vo List.vo SetoidList.vo \ - ListTactics.vo ) - -STRINGSVO:=$(addprefix theories/Strings/, \ - Ascii.vo String.vo ) - -SETSVO:=$(addprefix theories/Sets/, \ - Classical_sets.vo Permut.vo \ - Constructive_sets.vo Powerset.vo \ - Cpo.vo Powerset_Classical_facts.vo \ - Ensembles.vo Powerset_facts.vo \ - Finite_sets.vo Relations_1.vo \ - Finite_sets_facts.vo Relations_1_facts.vo \ - Image.vo Relations_2.vo \ - Infinite_sets.vo Relations_2_facts.vo \ - Integers.vo Relations_3.vo \ - Multiset.vo Relations_3_facts.vo \ - Partial_Order.vo Uniset.vo ) - -FSETSBASEVO:=$(addprefix theories/FSets/, \ - FSetInterface.vo FSetList.vo FSetBridge.vo \ - FSetFacts.vo FSetProperties.vo FSetEqProperties.vo \ - FSetWeakList.vo FSetAVL.vo FSetDecide.vo \ - FSetCompat.vo FSets.vo \ - FMapInterface.vo FMapList.vo FMapFacts.vo \ - FMapWeakList.vo FMapPositive.vo FSetToFiniteSet.vo \ - FMaps.vo ) - -FSETS_basic:= - -FSETS_all:=$(addprefix theories/FSets/, \ - FMapAVL.vo FMapFullAVL.vo ) - - -FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS)) - -ALLFSETS:=$(FSETSBASEVO) $(FSETS_all) - -MSETSVO:=$(addprefix theories/MSets/, \ - MSetInterface.vo MSetList.vo \ - MSetFacts.vo MSetProperties.vo MSetEqProperties.vo \ - MSetWeakList.vo MSetAVL.vo MSetDecide.vo \ - MSets.vo MSetToFiniteSet.vo) - -RELATIONSVO:=$(addprefix theories/Relations/, \ - Operators_Properties.vo Relation_Definitions.vo \ - Relation_Operators.vo Relations.vo ) - -WELLFOUNDEDVO:=$(addprefix theories/Wellfounded/, \ - Disjoint_Union.vo Inclusion.vo Inverse_Image.vo \ - Transitive_Closure.vo Union.vo Wellfounded.vo \ - Well_Ordering.vo Lexicographic_Product.vo \ - Lexicographic_Exponentiation.vo ) - -REALSBASEVO:=$(addprefix theories/Reals/, \ - Rdefinitions.vo Raxioms.vo RIneq.vo DiscrR.vo \ - Rbase.vo LegacyRfield.vo Rpow_def.vo ) - -REALS_basic:= - -REALS_all:=$(addprefix theories/Reals/, \ - R_Ifp.vo Rbasic_fun.vo R_sqr.vo SplitAbsolu.vo \ - SplitRmult.vo ArithProp.vo Rfunctions.vo Rseries.vo \ - SeqProp.vo Rcomplete.vo PartSum.vo AltSeries.vo \ - Binomial.vo Rsigma.vo Rprod.vo Cauchy_prod.vo \ - Alembert.vo SeqSeries.vo Rtrigo_fun.vo Rtrigo_def.vo \ - Rtrigo_alt.vo Cos_rel.vo Cos_plus.vo Rtrigo.vo \ - Rlimit.vo Rderiv.vo RList.vo Ranalysis1.vo \ - Ranalysis2.vo Ranalysis3.vo Rtopology.vo MVT.vo \ - PSeries_reg.vo Exp_prop.vo Rtrigo_reg.vo Rsqrt_def.vo \ - R_sqrt.vo Rtrigo_calc.vo Rgeom.vo Sqrt_reg.vo \ - Ranalysis4.vo Rpower.vo Ranalysis.vo NewtonInt.vo \ - RiemannInt_SF.vo RiemannInt.vo Integration.vo \ - Rlogic.vo Reals.vo ROrderedType.vo Rminmax.vo ) - -REALSVO:=$(REALSBASEVO) $(REALS_$(REALS)) - -ALLREALS:=$(REALSBASEVO) $(REALS_all) - -NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \ - NaryFunctions.vo NumPrelude.vo BigNumPrelude.vo ) - -CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \ - CyclicAxioms.vo NZCyclic.vo ) - -CYCLICINT31VO:=$(addprefix theories/Numbers/Cyclic/Int31/, \ - Int31.vo Cyclic31.vo ) - -CYCLICDOUBLECYCLICVO:=$(addprefix theories/Numbers/Cyclic/DoubleCyclic/, \ - DoubleType.vo DoubleBase.vo DoubleAdd.vo DoubleSub.vo \ - DoubleMul.vo DoubleDivn1.vo DoubleDiv.vo DoubleSqrt.vo \ - DoubleLift.vo DoubleCyclic.vo ) - -CYCLICZMODULOVO := $(addprefix theories/Numbers/Cyclic/ZModulo/, \ - ZModulo.vo ) - -CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO) \ - $(CYCLICZMODULOVO) - -NATINTVO:=$(addprefix theories/Numbers/NatInt/, \ - NZAxioms.vo NZBase.vo NZAdd.vo NZMul.vo \ - NZOrder.vo NZAddOrder.vo NZMulOrder.vo NZProperties.vo) - -NATURALABSTRACTVO:=$(addprefix theories/Numbers/Natural/Abstract/, \ - NAxioms.vo NBase.vo NAdd.vo \ - NOrder.vo NAddOrder.vo NMulOrder.vo NSub.vo \ - NProperties.vo NIso.vo NStrongRec.vo NDefOps.vo) - -NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \ - NPeano.vo ) - -NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \ - NBinary.vo ) - -NATURALSPECVIAZVO:=$(addprefix theories/Numbers/Natural/SpecViaZ/, \ - NSig.vo NSigNAxioms.vo ) - -NATURALBIGNVO:=$(addprefix theories/Numbers/Natural/BigN/, \ - Nbasic.vo NMake.vo BigN.vo ) - -NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \ - $(NATURALSPECVIAZVO) $(NATURALBIGNVO) - -INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \ - ZAxioms.vo ZBase.vo ZAdd.vo ZMul.vo \ - ZLt.vo ZAddOrder.vo ZMulOrder.vo ZProperties.vo) - -INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \ - ZBinary.vo ) - -INTEGERNATPAIRSVO:=$(addprefix theories/Numbers/Integer/NatPairs/, \ - ZNatPairs.vo ) - -INTEGERSPECVIAZVO:=$(addprefix theories/Numbers/Integer/SpecViaZ/, \ - ZSig.vo ZSigZAxioms.vo ) - -INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \ - ZMake.vo BigZ.vo ) - -INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \ - $(INTEGERSPECVIAZVO) $(INTEGERBIGZVO) - -RATIONALSPECVIAQVO:=$(addprefix theories/Numbers/Rational/SpecViaQ/, \ - QSig.vo ) - -RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \ - QMake.vo BigQ.vo ) - -RATIONALVO:=$(RATIONALSPECVIAQVO) $(RATIONALBIGQVO) +## we now retrieve the names of .vo file to compile in */vo.itarget files -NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO) $(CYCLICVO) $(RATIONALVO) +cat_vo_itarget = $(addprefix $(1)/,$(shell cat $(1)/vo.itarget)) -SETOIDSVO:=$(addprefix theories/Setoids/, \ - Setoid.vo ) - -UNICODEVO:=$(addprefix theories/Unicode/, \ - Utf8.vo ) - -CLASSESVO:=$(addprefix theories/Classes/, \ - Init.vo RelationClasses.vo Morphisms.vo Morphisms_Prop.vo \ - Morphisms_Relations.vo Functions.vo Equivalence.vo SetoidTactics.vo \ - SetoidClass.vo SetoidAxioms.vo EquivDec.vo SetoidDec.vo \ - RelationPairs.vo ) +## Theories -PROGRAMVO:=$(addprefix theories/Program/, \ - Tactics.vo Equality.vo Subset.vo Utils.vo \ - Wf.vo Basics.vo Combinators.vo Syntax.vo Program.vo ) +INITVO:=$(call cat_vo_itarget, theories/Init) +LOGICVO:=$(call cat_vo_itarget, theories/Logic) +STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures) +ARITHVO:=$(call cat_vo_itarget, theories/Arith) +SORTINGVO:=$(call cat_vo_itarget, theories/Sorting) +BOOLVO:=$(call cat_vo_itarget, theories/Bool) +NARITHVO:=$(call cat_vo_itarget, theories/NArith) +ZARITHVO:=$(call cat_vo_itarget, theories/ZArith) +QARITHVO:=$(call cat_vo_itarget, theories/QArith) +LISTSVO:=$(call cat_vo_itarget, theories/Lists) +STRINGSVO:=$(call cat_vo_itarget, theories/Strings) +SETSVO:=$(call cat_vo_itarget, theories/Sets) +FSETSVO:=$(call cat_vo_itarget, theories/FSets) +MSETSVO:=$(call cat_vo_itarget, theories/MSets) +RELATIONSVO:=$(call cat_vo_itarget, theories/Relations) +WELLFOUNDEDVO:=$(call cat_vo_itarget, theories/Wellfounded) +REALSVO:=$(call cat_vo_itarget, theories/Reals) +NUMBERSVO:=$(call cat_vo_itarget, theories/Numbers) +SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids) +UNICODEVO:=$(call cat_vo_itarget, theories/Unicode) +CLASSESVO:=$(call cat_vo_itarget, theories/Classes) +PROGRAMVO:=$(call cat_vo_itarget, theories/Program) THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ @@ -515,70 +311,24 @@ THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO) ## Plugins -OMEGAVO:=$(addprefix plugins/omega/, \ - PreOmega.vo OmegaLemmas.vo OmegaPlugin.vo Omega.vo ) - -ROMEGAVO:=$(addprefix plugins/romega/, \ - ReflOmegaCore.vo ROmega.vo ) - -MICROMEGAVO:=$(addprefix plugins/micromega/, \ - CheckerMaker.vo Refl.vo \ - Env.vo RingMicromega.vo \ - EnvRing.vo VarMap.vo \ - OrderedRing.vo ZCoeff.vo \ - Psatz.vo ZMicromega.vo \ - QMicromega.vo RMicromega.vo \ - Tauto.vo ) - -QUOTEVO:=$(addprefix plugins/quote/, \ - Quote.vo ) - -RINGVO:=$(addprefix plugins/ring/, \ - LegacyArithRing.vo Ring_normalize.vo \ - LegacyRing_theory.vo LegacyRing.vo \ - LegacyNArithRing.vo \ - LegacyZArithRing.vo Ring_abstract.vo \ - Setoid_ring_normalize.vo \ - Setoid_ring.vo Setoid_ring_theory.vo ) - -FIELDVO:=$(addprefix plugins/field/, \ - LegacyField_Compl.vo LegacyField_Theory.vo \ - LegacyField_Tactic.vo LegacyField.vo ) - -NEWRINGVO:=$(addprefix plugins/setoid_ring/, \ - BinList.vo Ring_theory.vo \ - Ring_polynom.vo Ring_tac.vo \ - Ring_base.vo InitialRing.vo \ - Ring_equiv.vo Ring.vo \ - ArithRing.vo NArithRing.vo \ - ZArithRing.vo \ - Field_theory.vo Field_tac.vo \ - Field.vo RealField.vo ) - -GBVO:=$(addprefix plugins/groebner/, \ - GroebnerR.vo GroebnerZ.vo ) - -XMLVO:= - -FOURIERVO:=$(addprefix plugins/fourier/, \ - Fourier_util.vo Fourier.vo ) - -FUNINDVO:= - -RECDEFVO:=$(addprefix plugins/funind/, \ - Recdef.vo ) - +OMEGAVO:=$(call cat_vo_itarget, plugins/omega) +ROMEGAVO:=$(call cat_vo_itarget, plugins/romega) +MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega) +QUOTEVO:=$(call cat_vo_itarget, plugins/quote) +RINGVO:=$(call cat_vo_itarget, plugins/ring) +FIELDVO:=$(call cat_vo_itarget, plugins/field) +NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) +GBVO:=$(call cat_vo_itarget, plugins/groebner) +FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) +FUNINDVO:=$(call cat_vo_itarget, plugins/funind) +DPVO:=$(call cat_vo_itarget, plugins/dp) +RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) +XMLVO:= CCVO:= -DPVO:=$(addprefix plugins/dp/, \ - Dp.vo ) - -RTAUTOVO:=$(addprefix plugins/rtauto/, \ - Bintree.vo Rtauto.vo ) - PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ + $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ $(GBVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) @@ -593,18 +343,16 @@ ALLMODS:=$(call vo_to_mod,$(ALLVO)) LIBFILES:=$(THEORIESVO) $(PLUGINSVO) LIBFILESLIGHT:=$(THEORIESLIGHTVO) -## Specials + +########################################################################### +# Miscellaneous +########################################################################### MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 - -########################################################################### -# Miscellaneous -########################################################################### - DATE=$(shell LANG=C date +"%B %Y") SOURCEDOCDIR=dev/source-doc @@ -627,7 +375,7 @@ endif ## Enumeration of targets that require being done at stage2 VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ - fsets allfsets relations wellfounded ints reals allreals \ + fsets relations wellfounded ints reals \ setoids sorting natural integer rational numbers noreal \ omega micromega ring setoid_ring dp xml extraction field fourier \ funind cc subtac rtauto diff --git a/config/Makefile.template b/config/Makefile.template index 4d45f1b4e..8864f52d0 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -135,12 +135,6 @@ COQDOCDIR="COQDOCDIRECTORY" # Win32 systems: true (actually strip is bogus) STRIP=STRIPCOMMAND -# Options for fsets (all/basic) -FSETS=FSETSOPT - -# Options for reals (all/basic) -REALS=REALSOPT - # CoqIde (no/byte/opt) HASCOQIDE=COQIDEOPT @@ -65,9 +65,6 @@ usage () { printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n" echo "-natdynlink (yes|no)" printf "\tSpecifies whether or not to use dynamic loading of native code\n" - echo "-fsets (all|basic)" - echo "-reals (all|basic)" - printf "\tSpecifies whether or not to compile full FSets/Reals library\n" echo "-coqide (opt|byte|no)" printf "\tSpecifies whether or not to compile Coqide\n" echo "-browser <command>" @@ -131,8 +128,6 @@ emacs_spec=no camldir_spec=no lablgtkdir_spec=no coqdocdir_spec=no -fsets=all -reals=all arch_spec=no coqide_spec=no browser_spec=no @@ -208,16 +203,6 @@ while : ; do *) natdynlink=no esac shift;; - -fsets|--fsets) case "$2" in - yes|all) fsets=all;; - *) fsets=basic - esac - shift;; - -reals|--reals) case "$2" in - yes|all) reals=all;; - *) reals=basic - esac - shift;; -coqide|--coqide) coqide_spec=yes case "$2" in byte|opt) COQIDE=$2;; @@ -852,16 +837,6 @@ fi if test "$COQIDE" != "no"; then echo " Lablgtk2 library in : $LABLGTKLIB" fi -if test "$fsets" = "all"; then -echo " FSets theory : All" -else -echo " FSets theory : Basic" -fi -if test "$reals" = "all"; then -echo " Reals theory : All" -else -echo " Reals theory : Basic" -fi if test "$with_doc" = "all"; then echo " Documentation : All" else @@ -1089,8 +1064,6 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|AREXEC|$ar_exec|" \ -e "s|RANLIBEXEC|$ranlib_exec|" \ -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ - -e "s|FSETSOPT|$fsets|" \ - -e "s|REALSOPT|$reals|" \ -e "s|COQIDEOPT|$COQIDE|" \ -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ -e "s|WITHDOCOPT|$with_doc|" \ diff --git a/myocamlbuild.ml b/myocamlbuild.ml index f7c014aba..18e73cc2e 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -120,17 +120,22 @@ let makeinitial = "states/MakeInitial.v" let nmake = "theories/Numbers/Natural/BigN/NMake.v" let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml" -let theoriesv = - let vo = string_list_of_file "theories/theories.itarget" in - List.map (fun s -> "theories/"^(Filename.chop_suffix s "o")) vo +let adapt_name (pref,oldsuf,newsuf) f = + pref ^ (Filename.chop_suffix f oldsuf) ^ newsuf -let pluginsv = - let vo = string_list_of_file "plugins/pluginsvo.itarget" in - List.map (fun s -> "plugins/"^(Filename.chop_suffix s "o")) vo +let get_names (oldsuf,newsuf) s = + let pref = Filename.dirname s ^ "/" in + List.map (adapt_name (pref,oldsuf,newsuf)) (string_list_of_file s) -let pluginsmllib = - let cma = string_list_of_file "plugins/pluginsbyte.itarget" in - List.map (fun s -> "plugins/"^(Filename.chop_suffix s ".cma")^".mllib") cma +let get_vo_itargets f = + let vo_itargets = get_names (".otarget",".itarget") f in + List.flatten (List.map (get_names (".vo",".v")) vo_itargets) + +let theoriesv = get_vo_itargets "theories/theories.itarget" + +let pluginsv = get_vo_itargets "plugins/pluginsvo.itarget" + +let pluginsmllib = get_names (".cma",".mllib") "plugins/pluginsbyte.itarget" (** for correct execution of coqdep_boot, source files should have been imported in _build (and NMake.v should have been created). *) diff --git a/plugins/dp/vo.itarget b/plugins/dp/vo.itarget new file mode 100644 index 000000000..4d282709d --- /dev/null +++ b/plugins/dp/vo.itarget @@ -0,0 +1 @@ +Dp.vo diff --git a/plugins/field/vo.itarget b/plugins/field/vo.itarget new file mode 100644 index 000000000..22b56f330 --- /dev/null +++ b/plugins/field/vo.itarget @@ -0,0 +1,4 @@ +LegacyField_Compl.vo +LegacyField_Tactic.vo +LegacyField_Theory.vo +LegacyField.vo diff --git a/plugins/fourier/vo.itarget b/plugins/fourier/vo.itarget new file mode 100644 index 000000000..87d82dacc --- /dev/null +++ b/plugins/fourier/vo.itarget @@ -0,0 +1,2 @@ +Fourier_util.vo +Fourier.vo diff --git a/plugins/funind/vo.itarget b/plugins/funind/vo.itarget new file mode 100644 index 000000000..33c968302 --- /dev/null +++ b/plugins/funind/vo.itarget @@ -0,0 +1 @@ +Recdef.vo diff --git a/plugins/groebner/vo.itarget b/plugins/groebner/vo.itarget new file mode 100644 index 000000000..ad9d0e4ef --- /dev/null +++ b/plugins/groebner/vo.itarget @@ -0,0 +1,2 @@ +GroebnerR.vo +GroebnerZ.vo diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget new file mode 100644 index 000000000..302013087 --- /dev/null +++ b/plugins/micromega/vo.itarget @@ -0,0 +1,13 @@ +CheckerMaker.vo +EnvRing.vo +Env.vo +OrderedRing.vo +Psatz.vo +QMicromega.vo +Refl.vo +RingMicromega.vo +RMicromega.vo +Tauto.vo +VarMap.vo +ZCoeff.vo +ZMicromega.vo diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget new file mode 100644 index 000000000..9d9a77a8c --- /dev/null +++ b/plugins/omega/vo.itarget @@ -0,0 +1,4 @@ +OmegaLemmas.vo +OmegaPlugin.vo +Omega.vo +PreOmega.vo diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget index 14c288005..d370e77dc 100644 --- a/plugins/pluginsvo.itarget +++ b/plugins/pluginsvo.itarget @@ -1,58 +1,12 @@ -dp/Dp.vo -field/LegacyField_Compl.vo -field/LegacyField_Tactic.vo -field/LegacyField_Theory.vo -field/LegacyField.vo -fourier/Fourier_util.vo -fourier/Fourier.vo -funind/Recdef.vo -groebner/GroebnerR.vo -groebner/GroebnerZ.vo -micromega/CheckerMaker.vo -micromega/EnvRing.vo -micromega/Env.vo -#micromega/MExtraction.vo (extraction of micromega.ml) -micromega/OrderedRing.vo -micromega/Psatz.vo -micromega/QMicromega.vo -micromega/Refl.vo -micromega/RingMicromega.vo -micromega/RMicromega.vo -micromega/Tauto.vo -micromega/VarMap.vo -micromega/ZCoeff.vo -micromega/ZMicromega.vo -omega/OmegaLemmas.vo -omega/OmegaPlugin.vo -omega/Omega.vo -omega/PreOmega.vo -quote/Quote.vo -ring/LegacyArithRing.vo -ring/LegacyNArithRing.vo -ring/LegacyRing_theory.vo -ring/LegacyRing.vo -ring/LegacyZArithRing.vo -ring/Ring_abstract.vo -ring/Ring_normalize.vo -ring/Setoid_ring_normalize.vo -ring/Setoid_ring_theory.vo -ring/Setoid_ring.vo -romega/ReflOmegaCore.vo -romega/ROmega.vo -rtauto/Bintree.vo -rtauto/Rtauto.vo -setoid_ring/ArithRing.vo -setoid_ring/BinList.vo -setoid_ring/Field_tac.vo -setoid_ring/Field_theory.vo -setoid_ring/Field.vo -setoid_ring/InitialRing.vo -setoid_ring/NArithRing.vo -setoid_ring/RealField.vo -setoid_ring/Ring_base.vo -setoid_ring/Ring_equiv.vo -setoid_ring/Ring_polynom.vo -setoid_ring/Ring_tac.vo -setoid_ring/Ring_theory.vo -setoid_ring/Ring.vo -setoid_ring/ZArithRing.vo +dp/vo.otarget +field/vo.otarget +fourier/vo.otarget +funind/vo.otarget +groebner/vo.otarget +micromega/vo.otarget +omega/vo.otarget +quote/vo.otarget +ring/vo.otarget +romega/vo.otarget +rtauto/vo.otarget +setoid_ring/vo.otarget diff --git a/plugins/quote/vo.itarget b/plugins/quote/vo.itarget new file mode 100644 index 000000000..7a44fc5aa --- /dev/null +++ b/plugins/quote/vo.itarget @@ -0,0 +1 @@ +Quote.vo
\ No newline at end of file diff --git a/plugins/ring/vo.itarget b/plugins/ring/vo.itarget new file mode 100644 index 000000000..da387be8c --- /dev/null +++ b/plugins/ring/vo.itarget @@ -0,0 +1,10 @@ +LegacyArithRing.vo +LegacyNArithRing.vo +LegacyRing_theory.vo +LegacyRing.vo +LegacyZArithRing.vo +Ring_abstract.vo +Ring_normalize.vo +Setoid_ring_normalize.vo +Setoid_ring_theory.vo +Setoid_ring.vo diff --git a/plugins/romega/vo.itarget b/plugins/romega/vo.itarget new file mode 100644 index 000000000..f7a3c41c7 --- /dev/null +++ b/plugins/romega/vo.itarget @@ -0,0 +1,2 @@ +ReflOmegaCore.vo +ROmega.vo diff --git a/plugins/rtauto/vo.itarget b/plugins/rtauto/vo.itarget new file mode 100644 index 000000000..4c9364ad7 --- /dev/null +++ b/plugins/rtauto/vo.itarget @@ -0,0 +1,2 @@ +Bintree.vo +Rtauto.vo diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget new file mode 100644 index 000000000..6934375bc --- /dev/null +++ b/plugins/setoid_ring/vo.itarget @@ -0,0 +1,15 @@ +ArithRing.vo +BinList.vo +Field_tac.vo +Field_theory.vo +Field.vo +InitialRing.vo +NArithRing.vo +RealField.vo +Ring_base.vo +Ring_equiv.vo +Ring_polynom.vo +Ring_tac.vo +Ring_theory.vo +Ring.vo +ZArithRing.vo diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget new file mode 100644 index 000000000..c3f29d214 --- /dev/null +++ b/theories/Arith/vo.itarget @@ -0,0 +1,23 @@ +Arith_base.vo +Arith.vo +Between.vo +Bool_nat.vo +Compare_dec.vo +Compare.vo +Div2.vo +EqNat.vo +Euclid.vo +Even.vo +Factorial.vo +Gt.vo +Le.vo +Lt.vo +Max.vo +Minus.vo +Min.vo +Mult.vo +Peano_dec.vo +Plus.vo +Wf_nat.vo +NatOrderedType.vo +MinMax.vo diff --git a/theories/Bool/vo.itarget b/theories/Bool/vo.itarget new file mode 100644 index 000000000..24cbf4edc --- /dev/null +++ b/theories/Bool/vo.itarget @@ -0,0 +1,7 @@ +BoolEq.vo +Bool.vo +Bvector.vo +DecBool.vo +IfProp.vo +Sumbool.vo +Zerob.vo diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget new file mode 100644 index 000000000..fcd3a77df --- /dev/null +++ b/theories/Classes/vo.itarget @@ -0,0 +1,13 @@ +Equivalence.vo +EquivDec.vo +Functions.vo +Init.vo +Morphisms_Prop.vo +Morphisms_Relations.vo +Morphisms.vo +RelationClasses.vo +SetoidAxioms.vo +SetoidClass.vo +SetoidDec.vo +SetoidTactics.vo +RelationPairs.vo diff --git a/theories/FSets/vo.itarget b/theories/FSets/vo.itarget new file mode 100644 index 000000000..67ef9585e --- /dev/null +++ b/theories/FSets/vo.itarget @@ -0,0 +1,20 @@ +FMapAVL.vo +FMapFacts.vo +FMapFullAVL.vo +FMapInterface.vo +FMapList.vo +FMapPositive.vo +FMaps.vo +FMapWeakList.vo +FSetCompat.vo +FSetAVL.vo +FSetBridge.vo +FSetDecide.vo +FSetEqProperties.vo +FSetFacts.vo +FSetInterface.vo +FSetList.vo +FSetProperties.vo +FSets.vo +FSetToFiniteSet.vo +FSetWeakList.vo diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget new file mode 100644 index 000000000..f53d55e71 --- /dev/null +++ b/theories/Init/vo.itarget @@ -0,0 +1,9 @@ +Datatypes.vo +Logic_Type.vo +Logic.vo +Notations.vo +Peano.vo +Prelude.vo +Specif.vo +Tactics.vo +Wf.vo diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget new file mode 100644 index 000000000..d2a31367d --- /dev/null +++ b/theories/Lists/vo.itarget @@ -0,0 +1,7 @@ +ListSet.vo +ListTactics.vo +List.vo +SetoidList.vo +StreamMemo.vo +Streams.vo +TheoryList.vo diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget new file mode 100644 index 000000000..460468977 --- /dev/null +++ b/theories/Logic/vo.itarget @@ -0,0 +1,28 @@ +Berardi.vo +ChoiceFacts.vo +ClassicalChoice.vo +ClassicalDescription.vo +ClassicalEpsilon.vo +ClassicalFacts.vo +Classical_Pred_Set.vo +Classical_Pred_Type.vo +Classical_Prop.vo +Classical_Type.vo +ClassicalUniqueChoice.vo +Classical.vo +ConstructiveEpsilon.vo +Decidable.vo +Description.vo +Diaconescu.vo +Epsilon.vo +Eqdep_dec.vo +EqdepFacts.vo +Eqdep.vo +FunctionalExtensionality.vo +Hurkens.vo +IndefiniteDescription.vo +JMeq.vo +ProofIrrelevanceFacts.vo +ProofIrrelevance.vo +RelationalChoice.vo +SetIsType.vo diff --git a/theories/MSets/vo.itarget b/theories/MSets/vo.itarget new file mode 100644 index 000000000..970d73d1f --- /dev/null +++ b/theories/MSets/vo.itarget @@ -0,0 +1,10 @@ +MSetAVL.vo +MSetDecide.vo +MSetEqProperties.vo +MSetFacts.vo +MSetInterface.vo +MSetList.vo +MSetProperties.vo +MSets.vo +MSetToFiniteSet.vo +MSetWeakList.vo diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget new file mode 100644 index 000000000..32f94f013 --- /dev/null +++ b/theories/NArith/vo.itarget @@ -0,0 +1,12 @@ +BinNat.vo +BinPos.vo +NArith.vo +Ndec.vo +Ndigits.vo +Ndist.vo +Nnat.vo +Pnat.vo +POrderedType.vo +Pminmax.vo +NOrderedType.vo +Nminmax.vo diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget new file mode 100644 index 000000000..b38d939c2 --- /dev/null +++ b/theories/Numbers/vo.itarget @@ -0,0 +1,61 @@ +BigNumPrelude.vo +Cyclic/Abstract/CyclicAxioms.vo +Cyclic/Abstract/NZCyclic.vo +Cyclic/DoubleCyclic/DoubleAdd.vo +Cyclic/DoubleCyclic/DoubleBase.vo +Cyclic/DoubleCyclic/DoubleCyclic.vo +Cyclic/DoubleCyclic/DoubleDivn1.vo +Cyclic/DoubleCyclic/DoubleDiv.vo +Cyclic/DoubleCyclic/DoubleLift.vo +Cyclic/DoubleCyclic/DoubleMul.vo +Cyclic/DoubleCyclic/DoubleSqrt.vo +Cyclic/DoubleCyclic/DoubleSub.vo +Cyclic/DoubleCyclic/DoubleType.vo +Cyclic/Int31/Cyclic31.vo +Cyclic/Int31/Int31.vo +Cyclic/ZModulo/ZModulo.vo +Integer/Abstract/ZAddOrder.vo +Integer/Abstract/ZAdd.vo +Integer/Abstract/ZAxioms.vo +Integer/Abstract/ZBase.vo +Integer/Abstract/ZLt.vo +Integer/Abstract/ZMulOrder.vo +Integer/Abstract/ZMul.vo +Integer/Abstract/ZProperties.vo +Integer/BigZ/BigZ.vo +Integer/BigZ/ZMake.vo +Integer/Binary/ZBinary.vo +Integer/NatPairs/ZNatPairs.vo +Integer/SpecViaZ/ZSig.vo +Integer/SpecViaZ/ZSigZAxioms.vo +NaryFunctions.vo +NatInt/NZAddOrder.vo +NatInt/NZAdd.vo +NatInt/NZAxioms.vo +NatInt/NZBase.vo +NatInt/NZMulOrder.vo +NatInt/NZMul.vo +NatInt/NZOrder.vo +NatInt/NZProperties.vo +Natural/Abstract/NAddOrder.vo +Natural/Abstract/NAdd.vo +Natural/Abstract/NAxioms.vo +Natural/Abstract/NBase.vo +Natural/Abstract/NDefOps.vo +Natural/Abstract/NIso.vo +Natural/Abstract/NMulOrder.vo +Natural/Abstract/NOrder.vo +Natural/Abstract/NStrongRec.vo +Natural/Abstract/NSub.vo +Natural/Abstract/NProperties.vo +Natural/BigN/BigN.vo +Natural/BigN/Nbasic.vo +Natural/BigN/NMake.vo +Natural/Binary/NBinary.vo +Natural/Peano/NPeano.vo +Natural/SpecViaZ/NSigNAxioms.vo +Natural/SpecViaZ/NSig.vo +NumPrelude.vo +Rational/BigQ/BigQ.vo +Rational/BigQ/QMake.vo +Rational/SpecViaQ/QSig.vo diff --git a/theories/Program/vo.itarget b/theories/Program/vo.itarget new file mode 100644 index 000000000..864c815ae --- /dev/null +++ b/theories/Program/vo.itarget @@ -0,0 +1,9 @@ +Basics.vo +Combinators.vo +Equality.vo +Program.vo +Subset.vo +Syntax.vo +Tactics.vo +Utils.vo +Wf.vo diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget new file mode 100644 index 000000000..bc13ae242 --- /dev/null +++ b/theories/QArith/vo.itarget @@ -0,0 +1,10 @@ +Qabs.vo +QArith_base.vo +QArith.vo +Qcanon.vo +Qfield.vo +Qpower.vo +Qreals.vo +Qreduction.vo +Qring.vo +Qround.vo diff --git a/theories/Reals/vo.itarget b/theories/Reals/vo.itarget new file mode 100644 index 000000000..bcd47a0b2 --- /dev/null +++ b/theories/Reals/vo.itarget @@ -0,0 +1,58 @@ +Alembert.vo +AltSeries.vo +ArithProp.vo +Binomial.vo +Cauchy_prod.vo +Cos_plus.vo +Cos_rel.vo +DiscrR.vo +Exp_prop.vo +Integration.vo +LegacyRfield.vo +MVT.vo +NewtonInt.vo +PartSum.vo +PSeries_reg.vo +Ranalysis1.vo +Ranalysis2.vo +Ranalysis3.vo +Ranalysis4.vo +Ranalysis.vo +Raxioms.vo +Rbase.vo +Rbasic_fun.vo +Rcomplete.vo +Rdefinitions.vo +Rderiv.vo +Reals.vo +Rfunctions.vo +Rgeom.vo +RiemannInt_SF.vo +RiemannInt.vo +R_Ifp.vo +RIneq.vo +Rlimit.vo +RList.vo +Rlogic.vo +Rpow_def.vo +Rpower.vo +Rprod.vo +Rseries.vo +Rsigma.vo +Rsqrt_def.vo +R_sqrt.vo +R_sqr.vo +Rtopology.vo +Rtrigo_alt.vo +Rtrigo_calc.vo +Rtrigo_def.vo +Rtrigo_fun.vo +Rtrigo_reg.vo +Rtrigo.vo +SeqProp.vo +SeqSeries.vo +SplitAbsolu.vo +SplitRmult.vo +Sqrt_reg.vo +ROrderedType.vo +Rminmax.vo diff --git a/theories/Relations/vo.itarget b/theories/Relations/vo.itarget new file mode 100644 index 000000000..9d81dd07a --- /dev/null +++ b/theories/Relations/vo.itarget @@ -0,0 +1,4 @@ +Operators_Properties.vo +Relation_Definitions.vo +Relation_Operators.vo +Relations.vo diff --git a/theories/Setoids/vo.itarget b/theories/Setoids/vo.itarget new file mode 100644 index 000000000..8d608cf75 --- /dev/null +++ b/theories/Setoids/vo.itarget @@ -0,0 +1 @@ +Setoid.vo
\ No newline at end of file diff --git a/theories/Sets/vo.itarget b/theories/Sets/vo.itarget new file mode 100644 index 000000000..9ebe92f52 --- /dev/null +++ b/theories/Sets/vo.itarget @@ -0,0 +1,22 @@ +Classical_sets.vo +Constructive_sets.vo +Cpo.vo +Ensembles.vo +Finite_sets_facts.vo +Finite_sets.vo +Image.vo +Infinite_sets.vo +Integers.vo +Multiset.vo +Partial_Order.vo +Permut.vo +Powerset_Classical_facts.vo +Powerset_facts.vo +Powerset.vo +Relations_1_facts.vo +Relations_1.vo +Relations_2_facts.vo +Relations_2.vo +Relations_3_facts.vo +Relations_3.vo +Uniset.vo diff --git a/theories/Sorting/vo.itarget b/theories/Sorting/vo.itarget new file mode 100644 index 000000000..b14f8f743 --- /dev/null +++ b/theories/Sorting/vo.itarget @@ -0,0 +1,5 @@ +Heap.vo +Permutation.vo +PermutEq.vo +PermutSetoid.vo +Sorting.vo diff --git a/theories/Strings/vo.itarget b/theories/Strings/vo.itarget new file mode 100644 index 000000000..20813b427 --- /dev/null +++ b/theories/Strings/vo.itarget @@ -0,0 +1,2 @@ +Ascii.vo +String.vo diff --git a/theories/Structures/vo.itarget b/theories/Structures/vo.itarget new file mode 100644 index 000000000..6500dcd89 --- /dev/null +++ b/theories/Structures/vo.itarget @@ -0,0 +1,15 @@ +OrderedTypeAlt.vo +OrderedTypeEx.vo +OrderedType.vo +DecidableType.vo +DecidableTypeEx.vo +OrderedType2Alt.vo +OrderedType2Ex.vo +OrderedType2.vo +OrderedType2Facts.vo +OrderedType2Lists.vo +DecidableType2.vo +DecidableType2Ex.vo +DecidableType2Facts.vo +OrderTac.vo +GenericMinMax.vo diff --git a/theories/Unicode/vo.itarget b/theories/Unicode/vo.itarget new file mode 100644 index 000000000..243a40b76 --- /dev/null +++ b/theories/Unicode/vo.itarget @@ -0,0 +1 @@ +Utf8.vo diff --git a/theories/Wellfounded/vo.itarget b/theories/Wellfounded/vo.itarget new file mode 100644 index 000000000..034d53106 --- /dev/null +++ b/theories/Wellfounded/vo.itarget @@ -0,0 +1,9 @@ +Disjoint_Union.vo +Inclusion.vo +Inverse_Image.vo +Lexicographic_Exponentiation.vo +Lexicographic_Product.vo +Transitive_Closure.vo +Union.vo +Wellfounded.vo +Well_Ordering.vo diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget new file mode 100644 index 000000000..471688fba --- /dev/null +++ b/theories/ZArith/vo.itarget @@ -0,0 +1,32 @@ +auxiliary.vo +BinInt.vo +Int.vo +Wf_Z.vo +Zabs.vo +ZArith_base.vo +ZArith_dec.vo +ZArith.vo +Zbinary.vo +Zbool.vo +Zcompare.vo +Zcomplements.vo +Zdiv.vo +Zeven.vo +Zgcd_alt.vo +Zhints.vo +Zlogarithm.vo +Zmax.vo +Zminmax.vo +Zmin.vo +Zmisc.vo +Znat.vo +Znumtheory.vo +ZOdiv_def.vo +ZOdiv.vo +Zorder.vo +Zpow_def.vo +Zpower.vo +Zpow_facts.vo +Zsqrt.vo +Zwf.vo +ZOrderedType.vo 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 |