aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.build10
-rw-r--r--Makefile.common340
-rw-r--r--config/Makefile.template6
-rwxr-xr-xconfigure27
-rw-r--r--myocamlbuild.ml23
-rw-r--r--plugins/dp/vo.itarget1
-rw-r--r--plugins/field/vo.itarget4
-rw-r--r--plugins/fourier/vo.itarget2
-rw-r--r--plugins/funind/vo.itarget1
-rw-r--r--plugins/groebner/vo.itarget2
-rw-r--r--plugins/micromega/vo.itarget13
-rw-r--r--plugins/omega/vo.itarget4
-rw-r--r--plugins/pluginsvo.itarget70
-rw-r--r--plugins/quote/vo.itarget1
-rw-r--r--plugins/ring/vo.itarget10
-rw-r--r--plugins/romega/vo.itarget2
-rw-r--r--plugins/rtauto/vo.itarget2
-rw-r--r--plugins/setoid_ring/vo.itarget15
-rw-r--r--theories/Arith/vo.itarget23
-rw-r--r--theories/Bool/vo.itarget7
-rw-r--r--theories/Classes/vo.itarget13
-rw-r--r--theories/FSets/vo.itarget20
-rw-r--r--theories/Init/vo.itarget9
-rw-r--r--theories/Lists/vo.itarget7
-rw-r--r--theories/Logic/vo.itarget28
-rw-r--r--theories/MSets/vo.itarget10
-rw-r--r--theories/NArith/vo.itarget12
-rw-r--r--theories/Numbers/vo.itarget61
-rw-r--r--theories/Program/vo.itarget9
-rw-r--r--theories/QArith/vo.itarget10
-rw-r--r--theories/Reals/vo.itarget58
-rw-r--r--theories/Relations/vo.itarget4
-rw-r--r--theories/Setoids/vo.itarget1
-rw-r--r--theories/Sets/vo.itarget22
-rw-r--r--theories/Sorting/vo.itarget5
-rw-r--r--theories/Strings/vo.itarget2
-rw-r--r--theories/Structures/vo.itarget15
-rw-r--r--theories/Unicode/vo.itarget1
-rw-r--r--theories/Wellfounded/vo.itarget9
-rw-r--r--theories/ZArith/vo.itarget32
-rw-r--r--theories/theories.itarget401
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
diff --git a/configure b/configure
index a2fc0e765..fad222fdb 100755
--- a/configure
+++ b/configure
@@ -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