Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo)

  Dealing with .vo files was harder than anticipated (issues with
  coqdep_boot and the location of the .v files). Current solution
  cannot compete for a beauty prize, but well.

  Several other issues remain (see top and bottom of myocamlbuild.ml)
  - For the moment the coqlib / coqsrc in Coq_config is to be
    hacked by hand to add _build/ in it.
  - Parallelism is a "no go" for the moment. Ocamlbuild accepts
    a -j option, but it has almost no effect experimentally.
    (but at least it doesn't take more time than make -j1,
     i.e. about 14 min here, instead of about 7 for make -j2)
  - After a first full build, ocamlbuild is awfully slow
    to detect that nothing has to be redone (1 min 25 here)

  To be continued...

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

4 files changed, 498 insertions, 62 deletions

diff --git a/bin.itarget b/bin.itarget
new file mode 100644
index 000000000..a4110bc95
--- /dev/null
+++ b/bin.itarget
@@ -0,0 +1,11 @@
+bin/coqmktop
+bin/coqtop
+bin/coqide
+bin/coqc
+bin/coqchk
+bin/coqdep
+bin/coqwc
+bin/coq-tex
+bin/coq_makefile
+bin/gallina
+bin/coqdoc
diff --git a/coq.itarget b/coq.itarget
index ea48c3339..6ab8e4670 100644
--- a/coq.itarget
+++ b/coq.itarget
@@ -1,12 +1,2 @@
-bin/coqmktop
-bin/coqtop
-bin/coqide
-bin/coqc
-bin/coqchk
-bin/coqdep
-bin/coqwc
-bin/coq-tex
-bin/coq_makefile
-bin/gallina
-bin/coqdoc
-states/initial.coq
+bin.otarget
+vo.otarget
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index ecc60c24b..3ad543302 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -5,28 +5,28 @@ open Ocamlbuild_pack
 open Printf
 open Scanf
 
-(** WARNING !! this is preliminary stuff, able only to build
-    coqtop.opt and coqtop.byte, and only in a precise environment
-    (ocaml 3.11 with natdynlink)
-
-    Support for other rules and other configurations will be
-    added later...
-
-    Usage: ./build   (which launches ocamlbuild coq.itarget)
-
-    Then you can (hopefully) launch coq (with no input state) via:
+(** WARNING !! this is preliminary stuff. It should allows you to
+    build coq and its libraries if everything goes right.
+    Support for all the build rules and configuration options
+    is progressively added. Tested only on linux + ocaml 3.11 +
+    natdynlink for now.
+
+    Usage: 
+     ./configure -local -opt
+     manual addition of /_build to coqlib and coqsrc in config/coq_config.ml
+     ./build   (which launches ocamlbuild coq.otarget)
+
+    Then you can (hopefully) launch coq via:
     
-    bin/coqtop.opt -nois -coqlib .
+    _build/bin/coqtop.opt
 
     or
 
     export CAML_LD_LIBRARY_PATH=_build/kernel/byterun 
-    bin/coqtop.byte -nois -coqlib .
+    _build/bin/coqtop.byte -nois
 
-    Apart from binaries in bin/, every created files are in _build.
+    Every created files are in _build.
     A "./build clean" should give you back a clean source tree
- 
-    TODO: understand how to create the right symlinks towards _build ...
 
 *)
 
@@ -78,6 +78,7 @@ let _ = Options.ocamlopt := A(get_env "OCAMLOPT")
 let _ = Options.ocamlyacc := A(get_env "OCAMLYACC")
 let _ = Options.ocamllex := A(get_env "OCAMLLEX")
 
+let ocaml = A(get_env "OCAML")
 let camlp4o = A(get_env "CAMLP4O")
 let camlp4incl = S[A"-I"; A(get_env "MYCAMLP4LIB")]
 let camlp4compat = Sh(get_env "CAMLP4COMPAT")
@@ -93,6 +94,7 @@ let lablgtkincl = Sh(get_env "COQIDEINCLUDES")
 let readable_genml = false
 let readable_flag = if readable_genml then A"pr_o.cmo" else N
 
+let _build = Options.build_dir
 
 
 (** Abbreviations about files *)
@@ -145,8 +147,12 @@ let initialcoq = "states/initial.coq"
 let init_vo = ["theories/Init/Prelude.vo";"theories/Init/Logic_Type.vo"]
 let makeinitial = "states/MakeInitial.v"
 
+let nmake = "theories/Numbers/Natural/BigN/NMake.v"
+let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml"
+
+let genvfiles = [nmake]
 
-(** A few common rules *)
+(** A few common functions *)
 
 let copy_rule src dst =
   rule (src^"_"^dst) ~dep:src ~prod:dst (fun _ _ -> cp src dst)
@@ -162,17 +168,26 @@ let copy_bin_best src dst = copy_rule (src^best_oext) dst
 
 let incl f = Ocaml_utils.ocaml_include_flags f
 
-
-
 (** The real game ... *)
 
 let _ = dispatch begin function
  | After_rules ->  (* Add our rules after the standard ones. *)
 
-(** The _build/bin directory isn't done by default *)
+(** We "pre-create" a few subdirs in _build to please coqtop *)
+
+     Shell.mkdir_p (!_build^"/bin");
+     Shell.mkdir_p (!_build^"/dev");
+
+(** Moreover, we "pre-import" in _build the sources file that will be needed
+    by coqdep_boot *)
 
-     if not (Sys.file_exists "_build/bin") then
-       Command.execute ~quiet:true (ln_s "../bin" "_build");
+     (*TODO: do something nicer than this call to find (maybe with Slurp) *)
+
+     let exclude = "-name _\\$* -or -name .\\* -prune -or" in
+     Command.execute ~quiet:true (Cmd (Sh
+       ("for i in `find theories plugins "^exclude^" -print`; do "^
+	"[ -f $i -a ! -f _build/$i ] && mkdir -p _build/`dirname $i` && cp $i _build/$i; "^
+	"done; true")));
 
 (** Camlp4 extensions *)
 
@@ -301,44 +316,40 @@ let _ = dispatch begin function
 
 (** Coq files dependencies *)
 
-     rule ".v.depends" ~prod:"%.v.depends" ~deps:["%.v";coqdep_boot]
+     rule ".v.d" ~prod:"%.v.depends" ~deps:(["%.v";coqdep_boot]@genvfiles)
        (fun env _ ->
 	  let v = env "%.v" and vd = env "%.v.depends" in
-	  (** All .v files are not necessarily present yet in _build
-	      (could we do something cleaner ?) *)
-	  Cmd (S [Sh "cd .. && ";
-		  P coqdep_boot;dep_dynlink;A"-slash";P v;Sh">";
-		  P ("_build/"^vd)]));
+	  (** NB: this relies on all .v files being already in _build. *)
+	  Cmd (S [P coqdep_boot;dep_dynlink;A"-slash";P v;Sh">";P vd]));
 
 (** Coq files compilation *)
 
-     let check_dep_coq vd v vo vg build =
-       (** NB: this rely on coqdep producing a single Makefile rule
-	   for one .v file *)
-       match string_list_of_file vd with
-	 | vo'::vg'::v'::deps when vo'=vo && vg'=vg^":" && v'=v ->
-	     let d = List.map (fun a -> [a]) deps in
+     let coq_build_dep f build =
+       (** NB: this relies on coqdep producing a single Makefile line
+	   for one .v file, with some specific shape : *)
+       match string_list_of_file (f^".v.depends") with
+	 | vo::vg::v::deps when vo=f^".vo" && vg=f^".glob:" && v=f^".v" ->
+	     let d = List.map (fun x -> [x]) deps in
 	     List.iter Outcome.ignore_good (build d)
-	 | _ -> failwith ("Something wrong with dependencies of "^v)
+	 | _ -> failwith ("Something wrong with dependencies of "^f^".v")
      in
 
-     let coq_v_rule d boot =
-       rule (d^"/.v.vo") ~prods:[d^"%.vo";d^"%.glob"]
-	 ~deps:([d^"%.v";d^"%.v.depends"]@(if boot then [] else [initialcoq]))
+     let coq_v_rule d init =
+       let bootflag = if init then A"-nois" else N in
+       let gendeps = if init then [coqtop] else [coqtop;initialcoq] in
+       rule (d^".v.vo")
+	 ~prods:[d^"%.vo";d^"%.glob"] ~deps:([d^"%.v";d^"%.v.depends"]@gendeps)
 	 (fun env build ->
-	    let v = env (d^"%") and vd = env (d^"%.v.depends") and
-		vo = env (d^"%.vo") and vg = env (d^"%.glob") in
-	    check_dep_coq vd (v^".v") vo vg build;
-	    let bootflag = if boot then S [A"-boot";A"-nois"] else N in
-	    Cmd (S [P coqtop;Sh "-coqlib .";bootflag; A"-compile";P v]))
+	    let f = env (d^"%") in
+	    coq_build_dep f build;
+	    Cmd (S [P coqtop;A"-boot";bootflag;A"-compile";P f]))
      in
      coq_v_rule "theories/Init/" true;
      coq_v_rule "" false;
 
      rule "initial.coq" ~prod:initialcoq ~deps:(makeinitial :: init_vo)
        (fun _ _ ->
-	  Cmd (S [P coqtop;Sh "-coqlib .";
-		  A"-batch";A"-nois";A"-notop";A"-silent";
+	  Cmd (S [P coqtop;A"-boot";A"-batch";A"-nois";A"-notop";A"-silent";
 		  A"-l";P makeinitial; A"-outputstate";P initialcoq]));
 
 (** Generation of _plugin_mod.ml files *)
@@ -357,15 +368,32 @@ let _ = dispatch begin function
 	  Cmd (S [!Options.ocamlopt;A"-linkall";A"-shared";
 		  A"-o";P (env "%.cmxs"); P (env "%.cmxa")]));
 
+(** Generation of NMake.v from NMake_gen.ml *)
+
+     rule "NMake" ~prod:nmake ~dep:nmakegen
+       (fun _ _ -> Cmd (S [ocaml;P nmakegen;Sh ">";P nmake]));
+
  | _ -> ()
 
 end
 
-(** TODO: 
-    * pourquoi certains binaires de bin/ se retrouvent parfois
-       avec une taille a zero ?
-    * les binaires n'ont pas l'air d'etre refait si on touche un fichier
-       (p.ex. coqdep_boot.ml)
-    * on repasse tout en revue sans arret, et c'est long (meme cached)...
+(** TODO / Remarques:
+
+    * L'idée initiale de partager bin/ et _build/bin/ a coup de symlink
+      etait une anerie : ocamlbuild prenait bin/foo comme _source_
+      et le copiait dans _build/bin/ (par dessus foo), ce qui donnait un
+      foo vide.
+
+    ==> Pour l'instant, les binaires sont dans _build/bin uniquement.
+    Une solution serait d'avoir deux repertoires de noms differents:
+    bin/ et _build/binaries/ par exemple.
+
+    * On repasse tout en revue sans arret, et c'est long, meme cached:
+      1 min 25 pour les 2662 targets en cache. 
+      Peut-on mieux faire ?
+
+    * coqdep a besoin dans _build des fichiers dont on depend,
+      mais ils n'y sont pas forcement, d'ou un gros cp au debut.
+      Y-a-t'il mieux à faire ?
 
 *)
diff --git a/vo.itarget b/vo.itarget
new file mode 100644
index 000000000..d322b96c3
--- /dev/null
+++ b/vo.itarget
@@ -0,0 +1,407 @@
+theories/Arith/Arith_base.vo
+theories/Arith/Arith.vo
+theories/Arith/Between.vo
+theories/Arith/Bool_nat.vo
+theories/Arith/Compare_dec.vo
+theories/Arith/Compare.vo
+theories/Arith/Div2.vo
+theories/Arith/EqNat.vo
+theories/Arith/Euclid.vo
+theories/Arith/Even.vo
+theories/Arith/Factorial.vo
+theories/Arith/Gt.vo
+theories/Arith/Le.vo
+theories/Arith/Lt.vo
+theories/Arith/Max.vo
+theories/Arith/Minus.vo
+theories/Arith/Min.vo
+theories/Arith/Mult.vo
+theories/Arith/Peano_dec.vo
+theories/Arith/Plus.vo
+theories/Arith/Wf_nat.vo
+
+theories/Bool/BoolEq.vo
+theories/Bool/Bool.vo
+theories/Bool/Bvector.vo
+theories/Bool/DecBool.vo
+theories/Bool/IfProp.vo
+theories/Bool/Sumbool.vo
+theories/Bool/Zerob.vo
+
+theories/Classes/Equivalence.vo
+theories/Classes/EquivDec.vo
+theories/Classes/Functions.vo
+theories/Classes/Init.vo
+theories/Classes/Morphisms_Prop.vo
+theories/Classes/Morphisms_Relations.vo
+theories/Classes/Morphisms.vo
+theories/Classes/RelationClasses.vo
+theories/Classes/SetoidAxioms.vo
+theories/Classes/SetoidClass.vo
+theories/Classes/SetoidDec.vo
+theories/Classes/SetoidTactics.vo
+
+theories/FSets/FMapAVL.vo
+theories/FSets/FMapFacts.vo
+theories/FSets/FMapFullAVL.vo
+theories/FSets/FMapInterface.vo
+theories/FSets/FMapList.vo
+theories/FSets/FMapPositive.vo
+theories/FSets/FMaps.vo
+theories/FSets/FMapWeakList.vo
+theories/FSets/FSetAVL.vo
+theories/FSets/FSetBridge.vo
+theories/FSets/FSetDecide.vo
+theories/FSets/FSetEqProperties.vo
+theories/FSets/FSetFacts.vo
+theories/FSets/FSetFullAVL.vo
+theories/FSets/FSetInterface.vo
+theories/FSets/FSetList.vo
+theories/FSets/FSetProperties.vo
+theories/FSets/FSets.vo
+theories/FSets/FSetToFiniteSet.vo
+theories/FSets/FSetWeakList.vo
+theories/FSets/OrderedTypeAlt.vo
+theories/FSets/OrderedTypeEx.vo
+theories/FSets/OrderedType.vo
+
+theories/Init/Datatypes.vo
+theories/Init/Logic_Type.vo
+theories/Init/Logic.vo
+theories/Init/Notations.vo
+theories/Init/Peano.vo
+theories/Init/Prelude.vo
+theories/Init/Specif.vo
+theories/Init/Tactics.vo
+theories/Init/Wf.vo
+
+theories/Lists/ListSet.vo
+theories/Lists/ListTactics.vo
+theories/Lists/List.vo
+theories/Lists/MonoList.vo
+theories/Lists/SetoidList.vo
+theories/Lists/StreamMemo.vo
+theories/Lists/Streams.vo
+theories/Lists/TheoryList.vo
+
+theories/Logic/Berardi.vo
+theories/Logic/ChoiceFacts.vo
+theories/Logic/ClassicalChoice.vo
+theories/Logic/ClassicalDescription.vo
+theories/Logic/ClassicalEpsilon.vo
+theories/Logic/ClassicalFacts.vo
+theories/Logic/Classical_Pred_Set.vo
+theories/Logic/Classical_Pred_Type.vo
+theories/Logic/Classical_Prop.vo
+theories/Logic/Classical_Type.vo
+theories/Logic/ClassicalUniqueChoice.vo
+theories/Logic/Classical.vo
+theories/Logic/ConstructiveEpsilon.vo
+theories/Logic/DecidableTypeEx.vo
+theories/Logic/DecidableType.vo
+theories/Logic/Decidable.vo
+theories/Logic/Description.vo
+theories/Logic/Diaconescu.vo
+theories/Logic/Epsilon.vo
+theories/Logic/Eqdep_dec.vo
+theories/Logic/EqdepFacts.vo
+theories/Logic/Eqdep.vo
+theories/Logic/FunctionalExtensionality.vo
+theories/Logic/Hurkens.vo
+theories/Logic/IndefiniteDescription.vo
+theories/Logic/JMeq.vo
+theories/Logic/ProofIrrelevanceFacts.vo
+theories/Logic/ProofIrrelevance.vo
+theories/Logic/RelationalChoice.vo
+theories/Logic/SetIsType.vo
+
+theories/NArith/BinNat.vo
+theories/NArith/BinPos.vo
+theories/NArith/NArith.vo
+theories/NArith/Ndec.vo
+theories/NArith/Ndigits.vo
+theories/NArith/Ndist.vo
+theories/NArith/Nnat.vo
+theories/NArith/Pnat.vo
+
+theories/Numbers/BigNumPrelude.vo
+theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
+theories/Numbers/Cyclic/Abstract/NZCyclic.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
+theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
+theories/Numbers/Cyclic/Int31/Cyclic31.vo
+theories/Numbers/Cyclic/Int31/Int31.vo
+theories/Numbers/Cyclic/ZModulo/ZModulo.vo
+theories/Numbers/Integer/Abstract/ZAddOrder.vo
+theories/Numbers/Integer/Abstract/ZAdd.vo
+theories/Numbers/Integer/Abstract/ZAxioms.vo
+theories/Numbers/Integer/Abstract/ZBase.vo
+#theories/Numbers/Integer/Abstract/ZDomain.vo
+theories/Numbers/Integer/Abstract/ZLt.vo
+theories/Numbers/Integer/Abstract/ZMulOrder.vo
+theories/Numbers/Integer/Abstract/ZMul.vo
+theories/Numbers/Integer/BigZ/BigZ.vo
+theories/Numbers/Integer/BigZ/ZMake.vo
+theories/Numbers/Integer/Binary/ZBinary.vo
+theories/Numbers/Integer/NatPairs/ZNatPairs.vo
+theories/Numbers/Integer/SpecViaZ/ZSig.vo
+theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo
+theories/Numbers/NaryFunctions.vo
+theories/Numbers/NatInt/NZAddOrder.vo
+theories/Numbers/NatInt/NZAdd.vo
+theories/Numbers/NatInt/NZAxioms.vo
+theories/Numbers/NatInt/NZBase.vo
+theories/Numbers/NatInt/NZMulOrder.vo
+theories/Numbers/NatInt/NZMul.vo
+theories/Numbers/NatInt/NZOrder.vo
+theories/Numbers/Natural/Abstract/NAddOrder.vo
+theories/Numbers/Natural/Abstract/NAdd.vo
+theories/Numbers/Natural/Abstract/NAxioms.vo
+theories/Numbers/Natural/Abstract/NBase.vo
+#theories/Numbers/Natural/Abstract/NDefOps.vo
+theories/Numbers/Natural/Abstract/NIso.vo
+theories/Numbers/Natural/Abstract/NMulOrder.vo
+theories/Numbers/Natural/Abstract/NMul.vo
+theories/Numbers/Natural/Abstract/NOrder.vo
+#theories/Numbers/Natural/Abstract/NStrongRec.vo
+theories/Numbers/Natural/Abstract/NSub.vo
+theories/Numbers/Natural/BigN/BigN.vo
+theories/Numbers/Natural/BigN/Nbasic.vo
+theories/Numbers/Natural/Binary/NBinary.vo
+theories/Numbers/Natural/Binary/NBinDefs.vo
+theories/Numbers/Natural/Peano/NPeano.vo
+theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo
+theories/Numbers/Natural/SpecViaZ/NSig.vo
+theories/Numbers/NumPrelude.vo
+theories/Numbers/Rational/BigQ/BigQ.vo
+theories/Numbers/Rational/BigQ/QMake.vo
+theories/Numbers/Rational/SpecViaQ/QSig.vo
+
+theories/Program/Basics.vo
+theories/Program/Combinators.vo
+theories/Program/Equality.vo
+theories/Program/Program.vo
+theories/Program/Subset.vo
+theories/Program/Syntax.vo
+theories/Program/Tactics.vo
+theories/Program/Utils.vo
+theories/Program/Wf.vo
+
+theories/QArith/Qabs.vo
+theories/QArith/QArith_base.vo
+theories/QArith/QArith.vo
+theories/QArith/Qcanon.vo
+theories/QArith/Qfield.vo
+theories/QArith/Qpower.vo
+theories/QArith/Qreals.vo
+theories/QArith/Qreduction.vo
+theories/QArith/Qring.vo
+theories/QArith/Qround.vo
+
+theories/Reals/Alembert.vo
+theories/Reals/AltSeries.vo
+theories/Reals/ArithProp.vo
+theories/Reals/Binomial.vo
+theories/Reals/Cauchy_prod.vo
+theories/Reals/Cos_plus.vo
+theories/Reals/Cos_rel.vo
+theories/Reals/DiscrR.vo
+theories/Reals/Exp_prop.vo
+theories/Reals/Integration.vo
+theories/Reals/LegacyRfield.vo
+theories/Reals/MVT.vo
+theories/Reals/NewtonInt.vo
+theories/Reals/PartSum.vo
+theories/Reals/PSeries_reg.vo
+theories/Reals/Ranalysis1.vo
+theories/Reals/Ranalysis2.vo
+theories/Reals/Ranalysis3.vo
+theories/Reals/Ranalysis4.vo
+theories/Reals/Ranalysis.vo
+theories/Reals/Raxioms.vo
+theories/Reals/Rbase.vo
+theories/Reals/Rbasic_fun.vo
+theories/Reals/Rcomplete.vo
+theories/Reals/Rdefinitions.vo
+theories/Reals/Rderiv.vo
+theories/Reals/Reals.vo
+theories/Reals/Rfunctions.vo
+theories/Reals/Rgeom.vo
+theories/Reals/RiemannInt_SF.vo
+theories/Reals/RiemannInt.vo
+theories/Reals/R_Ifp.vo
+theories/Reals/RIneq.vo
+theories/Reals/Rlimit.vo
+theories/Reals/RList.vo
+theories/Reals/Rlogic.vo
+theories/Reals/Rpow_def.vo
+theories/Reals/Rpower.vo
+theories/Reals/Rprod.vo
+theories/Reals/Rseries.vo
+theories/Reals/Rsigma.vo
+theories/Reals/Rsqrt_def.vo
+theories/Reals/R_sqrt.vo
+theories/Reals/R_sqr.vo
+theories/Reals/Rtopology.vo
+theories/Reals/Rtrigo_alt.vo
+theories/Reals/Rtrigo_calc.vo
+theories/Reals/Rtrigo_def.vo
+theories/Reals/Rtrigo_fun.vo
+theories/Reals/Rtrigo_reg.vo
+theories/Reals/Rtrigo.vo
+theories/Reals/SeqProp.vo
+theories/Reals/SeqSeries.vo
+theories/Reals/SplitAbsolu.vo
+theories/Reals/SplitRmult.vo
+theories/Reals/Sqrt_reg.vo
+
+theories/Relations/Operators_Properties.vo
+theories/Relations/Relation_Definitions.vo
+theories/Relations/Relation_Operators.vo
+theories/Relations/Relations.vo
+
+theories/Setoids/Setoid.vo
+theories/Sets/Classical_sets.vo
+theories/Sets/Constructive_sets.vo
+theories/Sets/Cpo.vo
+theories/Sets/Ensembles.vo
+theories/Sets/Finite_sets_facts.vo
+theories/Sets/Finite_sets.vo
+theories/Sets/Image.vo
+theories/Sets/Infinite_sets.vo
+theories/Sets/Integers.vo
+theories/Sets/Multiset.vo
+theories/Sets/Partial_Order.vo
+theories/Sets/Permut.vo
+theories/Sets/Powerset_Classical_facts.vo
+theories/Sets/Powerset_facts.vo
+theories/Sets/Powerset.vo
+theories/Sets/Relations_1_facts.vo
+theories/Sets/Relations_1.vo
+theories/Sets/Relations_2_facts.vo
+theories/Sets/Relations_2.vo
+theories/Sets/Relations_3_facts.vo
+theories/Sets/Relations_3.vo
+theories/Sets/Uniset.vo
+
+theories/Sorting/Heap.vo
+theories/Sorting/Permutation.vo
+theories/Sorting/PermutEq.vo
+theories/Sorting/PermutSetoid.vo
+theories/Sorting/Sorting.vo
+
+theories/Strings/Ascii.vo
+theories/Strings/String.vo
+
+theories/Unicode/Utf8.vo
+
+theories/Wellfounded/Disjoint_Union.vo
+theories/Wellfounded/Inclusion.vo
+theories/Wellfounded/Inverse_Image.vo
+theories/Wellfounded/Lexicographic_Exponentiation.vo
+theories/Wellfounded/Lexicographic_Product.vo
+theories/Wellfounded/Transitive_Closure.vo
+theories/Wellfounded/Union.vo
+theories/Wellfounded/Wellfounded.vo
+theories/Wellfounded/Well_Ordering.vo
+
+theories/ZArith/auxiliary.vo
+theories/ZArith/BinInt.vo
+theories/ZArith/Int.vo
+theories/ZArith/Wf_Z.vo
+theories/ZArith/Zabs.vo
+theories/ZArith/ZArith_base.vo
+theories/ZArith/ZArith_dec.vo
+theories/ZArith/ZArith.vo
+theories/ZArith/Zbinary.vo
+theories/ZArith/Zbool.vo
+theories/ZArith/Zcompare.vo
+theories/ZArith/Zcomplements.vo
+theories/ZArith/Zdiv.vo
+theories/ZArith/Zeven.vo
+theories/ZArith/Zgcd_alt.vo
+theories/ZArith/Zhints.vo
+theories/ZArith/Zlogarithm.vo
+theories/ZArith/Zmax.vo
+theories/ZArith/Zminmax.vo
+theories/ZArith/Zmin.vo
+theories/ZArith/Zmisc.vo
+theories/ZArith/Znat.vo
+theories/ZArith/Znumtheory.vo
+theories/ZArith/ZOdiv_def.vo
+theories/ZArith/ZOdiv.vo
+theories/ZArith/Zorder.vo
+theories/ZArith/Zpow_def.vo
+theories/ZArith/Zpower.vo
+theories/ZArith/Zpow_facts.vo
+theories/ZArith/Zsqrt.vo
+theories/ZArith/Zwf.vo
+
+plugins/dp/Dp.vo
+plugins/field/LegacyField_Compl.vo
+plugins/field/LegacyField_Tactic.vo
+plugins/field/LegacyField_Theory.vo
+plugins/field/LegacyField.vo
+plugins/fourier/Fourier_util.vo
+plugins/fourier/Fourier.vo
+plugins/funind/Recdef.vo
+plugins/groebner/GroebnerR.vo
+plugins/groebner/GroebnerZ.vo
+plugins/interface/CoqInterface.vo
+#plugins/interface/CoqParser.vo  (should not be compiled)
+plugins/micromega/CheckerMaker.vo
+plugins/micromega/EnvRing.vo
+plugins/micromega/Env.vo
+plugins/micromega/MExtraction.vo
+plugins/micromega/OrderedRing.vo
+plugins/micromega/Psatz.vo
+plugins/micromega/QMicromega.vo
+plugins/micromega/Refl.vo
+plugins/micromega/RingMicromega.vo
+plugins/micromega/RMicromega.vo
+plugins/micromega/Tauto.vo
+plugins/micromega/VarMap.vo
+plugins/micromega/ZCoeff.vo
+plugins/micromega/ZMicromega.vo
+plugins/omega/OmegaLemmas.vo
+plugins/omega/OmegaPlugin.vo
+plugins/omega/Omega.vo
+plugins/omega/PreOmega.vo
+plugins/quote/Quote.vo
+plugins/ring/LegacyArithRing.vo
+plugins/ring/LegacyNArithRing.vo
+plugins/ring/LegacyRing_theory.vo
+plugins/ring/LegacyRing.vo
+plugins/ring/LegacyZArithRing.vo
+plugins/ring/Ring_abstract.vo
+plugins/ring/Ring_normalize.vo
+plugins/ring/Setoid_ring_normalize.vo
+plugins/ring/Setoid_ring_theory.vo
+plugins/ring/Setoid_ring.vo
+plugins/romega/ReflOmegaCore.vo
+plugins/romega/ROmega.vo
+plugins/rtauto/Bintree.vo
+plugins/rtauto/Rtauto.vo
+plugins/setoid_ring/ArithRing.vo
+plugins/setoid_ring/BinList.vo
+plugins/setoid_ring/Field_tac.vo
+plugins/setoid_ring/Field_theory.vo
+plugins/setoid_ring/Field.vo
+plugins/setoid_ring/InitialRing.vo
+plugins/setoid_ring/NArithRing.vo
+plugins/setoid_ring/RealField.vo
+plugins/setoid_ring/Ring_base.vo
+plugins/setoid_ring/Ring_equiv.vo
+plugins/setoid_ring/Ring_polynom.vo
+plugins/setoid_ring/Ring_tac.vo
+plugins/setoid_ring/Ring_theory.vo
+plugins/setoid_ring/Ring.vo
+plugins/setoid_ring/ZArithRing.vo