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

23 files changed, 380 insertions, 379 deletions

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