From d1e8a2a6e5e2fdea6cf0ff0ed9860b98eced0c97 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 26 Mar 2009 19:31:40 +0000 Subject: 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 --- bin.itarget | 11 ++ coq.itarget | 14 +- myocamlbuild.ml | 128 +++++++++++------- vo.itarget | 407 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 498 insertions(+), 62 deletions(-) create mode 100644 bin.itarget create mode 100644 vo.itarget 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 -- cgit v1.2.3