Ocamlbuild: improvements suggested by N. Pouillard

 * Import of Coq_config via myocamlbuild_config.ml, instead of my get_env
 * As a consequence, we enrich this Coq_config with stuff that was
   only in config/Makefile
 * replace the big ugly find by some dependencies against source files
 * by the way: build csdpcert, with the right aliases.

I've tried to escape things properly for windows in ./configure,
but this isn't fully tested yet.

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

1 files changed, 348 insertions, 0 deletions

diff --git a/theories/theories.itarget b/theories/theories.itarget
new file mode 100644
index 000000000..7798ebebc
--- /dev/null
+++ b/theories/theories.itarget
@@ -0,0 +1,348 @@
+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
+
+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
+
+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/FSetAVL.vo
+FSets/FSetBridge.vo
+FSets/FSetDecide.vo
+FSets/FSetEqProperties.vo
+FSets/FSetFacts.vo
+FSets/FSetFullAVL.vo
+FSets/FSetInterface.vo
+FSets/FSetList.vo
+FSets/FSetProperties.vo
+FSets/FSets.vo
+FSets/FSetToFiniteSet.vo
+FSets/FSetWeakList.vo
+FSets/OrderedTypeAlt.vo
+FSets/OrderedTypeEx.vo
+FSets/OrderedType.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/MonoList.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/DecidableTypeEx.vo
+Logic/DecidableType.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
+
+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/ZDomain.vo
+Numbers/Integer/Abstract/ZLt.vo
+Numbers/Integer/Abstract/ZMulOrder.vo
+Numbers/Integer/Abstract/ZMul.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/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/NMul.vo
+Numbers/Natural/Abstract/NOrder.vo
+#Numbers/Natural/Abstract/NStrongRec.vo
+Numbers/Natural/Abstract/NSub.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/Binary/NBinDefs.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
+
+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