Factorisation between Makefile and ocamlbuild systems : .vo to compile are in */*/vo.itarget

 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7

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