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

11 files changed, 667 insertions, 580 deletions

diff --git a/build b/build
index 4552d5a43..26237b705 100755
--- a/build
+++ b/build
@@ -3,14 +3,20 @@
 FLAGS=
 OCAMLBUILD=ocamlbuild
 
+check_config() {
+ [ -f config/coq_config.ml ] || (echo "please run ./configure first"; exit 1)
+ [ -L myocamlbuild_config.ml ] || ln -sf config/coq_config.ml myocamlbuild_config.ml
+}
+
 ocb()
 {
+  check_config
   $OCAMLBUILD $FLAGS $*
 }
 
 rule() {
   case $1 in
-    clean)  ocb -clean && rm -rf bin/*;;
+    clean)  ocb -clean && rm -rf bin/* && rm -f myocamlbuild_config.ml;;
     all)    ocb coq.otarget;;
     *)      ocb $1;;
   esac;
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 7c80a96d4..3598b938d 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -13,12 +13,26 @@ val local : bool        (* local use (no installation) *)
 val coqlib : string     (* where the std library is installed *)
 val coqsrc : string     (* where are the sources *)
 
+val ocaml : string      (* names of ocaml binaries *)
+val ocamlc : string
+val ocamlopt : string
+val ocamlmklib : string
+val ocamldoc : string
+val ocamldep : string
+val ocamlyacc : string
+val ocamllex : string
+
 val camlbin : string    (* base directory of OCaml binaries *)
 val camllib : string    (* for Dynlink *)
 
 val camlp4 : string     (* exact name of camlp4: either "camlp4" ou "camlp5" *)
+val camlp4o : string    (* name of the camlp4o/camlp5o executable *)
 val camlp4bin : string  (* base directory for Camlp4/5 binaries *)
 val camlp4lib : string  (* where is the library of Camlp4 *)
+val camlp4compat : string (* compatibility argument to camlp4/5 *)
+
+val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *)
+val cflags : string     (* arguments passed to gcc *)
 
 val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
@@ -46,3 +60,4 @@ val browser : string
     variable COQREMOTEBROWSER *)
 
 val has_natdynlink : bool
+val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *)
diff --git a/configure b/configure
index 7b39eb422..894e43d64 100755
--- a/configure
+++ b/configure
@@ -875,9 +875,51 @@ echo "    documentation will be copied in $DOCDIR"
 echo "    emacs mode    will be copied in $EMACSLIB"
 echo ""
 
-#####################################################
-# Building the $COQTOP/config/coq_config.ml file
-#####################################################
+##################################################
+# Building the $COQTOP/dev/ocamldebug-coq file
+##################################################
+
+OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
+
+if test "$coq_debug_flag" = "-g" ; then
+  rm -f $OCAMLDEBUGCOQ
+  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
+      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
+      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
+      $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
+  chmod a-w,a+x $OCAMLDEBUGCOQ
+fi
+
+####################################################
+# Fixing lablgtk types (before/after 2.6.0) 
+####################################################
+
+if [ ! "$COQIDE" = "no" ]; then 
+    if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
+       if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
+        cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
+       else
+	cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
+       fi
+    else
+	cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
+    fi
+fi  
+
+##############################################
+# Creation of configuration files
+##############################################
+
+mlconfig_file="$COQSRC/config/coq_config.ml"
+config_file="$COQSRC/config/Makefile"
+config_template="$COQSRC/config/Makefile.template"
+
+
+### Warning !!
+### After this line, be careful when using variables,
+### since some of them (e.g. $COQSRC) will be escaped
+
 
 # An escaped version of a variable
 escape_var () {
@@ -888,65 +930,72 @@ EOF
 
 # Escaped version of browser command
 export BROWSER
-ESCBROWSER=`VAR=BROWSER escape_var`
+BROWSER=`VAR=BROWSER escape_var`
 
 # damned backslashes under M$Windows
 case $ARCH in
     win32)
-	ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
-	ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
-	ESCSRCDIR=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
-	ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
-  	ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
-  	ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-   	ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
-   	ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-   	ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
-	ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-	ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
-;;
-    *)
-        ESCCOQTOP="$COQTOP"
-	ESCBINDIR="$BINDIR"
-	ESCSRCDIR="$COQSRC"
-	ESCLIBDIR="$LIBDIR"
-	ESCCAMLDIR="$CAMLBIN"
-	ESCCAMLLIB="$CAMLLIB"
-  	ESCMANDIR="$MANDIR"
-  	ESCDOCDIR="$DOCDIR"
-   	ESCEMACSLIB="$EMACSLIB"
-   	ESCCOQDOCDIR="$COQDOCDIR"
-   	ESCCAMLP4BIN="$CAMLP4BIN"
-   	ESCCAMLP4LIB="$CAMLP4LIB"
-	ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
-	ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
-	ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS"
-	ESCBUILDLDPATH="$BUILDLDPATH"
-	;;
+	COQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
+	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+	COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
+	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+	CAMLBIN=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
+	CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
+	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+	DOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
+	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
+	COQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
+	CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
+	CAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
+	LABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
+	COQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
+	COQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
+	BUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
+	ocamlexec=`echo $ocamlexec |sed -e 's|\\\|\\\\\\\|g'`
+	bytecamlc=`echo $bytecamlc |sed -e 's|\\\|\\\\\\\|g'`
+	nativecamlc=`echo $nativecamlc |sed -e 's|\\\|\\\\\\\|g'`
+	ocamlmklibexec=`echo $ocamlmklibexec |sed -e 's|\\\|\\\\\\\|g'`
+	ocamldepexec=`echo $ocamldepexec |sed -e 's|\\\|\\\\\\\|g'`
+	ocamldocexec=`echo $ocamldocexec |sed -e 's|\\\|\\\\\\\|g'`
+	ocamllexexec=`echo $ocamllexexec |sed -e 's|\\\|\\\\\\\|g'`
+	ocamlyaccexec=`echo $ocamlyaccexec |sed -e 's|\\\|\\\\\\\|g'`
+	camlp4oexec=`echo $camlp4oexec |sed -e 's|\\\|\\\\\\\|g'`
+    ;;
 esac
 
-mlconfig_file="$COQSRC/config/coq_config.ml"
+#####################################################
+# Building the $COQTOP/config/coq_config.ml file
+#####################################################
+
 rm -f "$mlconfig_file"
 cat << END_OF_COQ_CONFIG > $mlconfig_file
 (* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
 
 let local = $local
-let coqrunbyteflags = "$ESCCOQRUNBYTEFLAGS"
-let coqlib = "$ESCLIBDIR"
-let coqsrc = "$ESCSRCDIR"
-let camlbin = "$ESCCAMLDIR"
-let camllib = "$ESCCAMLLIB"
+let coqrunbyteflags = "$COQRUNBYTEFLAGS"
+let coqlib = "$LIBDIR"
+let coqsrc = "$COQSRC"
+let ocaml = "$ocamlexec"
+let ocamlc = "$bytecamlc"
+let ocamlopt = "$nativecamlc"
+let ocamlmklib = "$ocamlmklibexec"
+let ocamldep = "$ocamldepexec"
+let ocamldoc = "$ocamldocexec"
+let ocamlyacc = "$ocamlyaccexec"
+let ocamllex = "$ocamllexexec"
+let camlbin = "$CAMLBIN"
+let camllib = "$CAMLLIB"
 let camlp4 = "$CAMLP4"
-let camlp4bin = "$ESCCAMLP4BIN"
-let camlp4lib = "$ESCCAMLP4LIB"
+let camlp4o = "$camlp4oexec"
+let camlp4bin = "$CAMLP4BIN"
+let camlp4lib = "$CAMLP4LIB"
+let camlp4compat = "$CAMLP4COMPAT"
+let coqideincl = "$LABLGTKINCLUDES"
+let cflags = "$cflags"
 let best = "$best_compiler"
 let arch = "$ARCH"
 let has_natdynlink = $HASNATDYNLINK
+let natdynlinkflag = "$NATDYNLINKFLAG"
 let osdeplibs = "$OSDEPLIBS"
 let version = "$VERSION"
 let caml_version = "$CAMLVERSION"
@@ -956,7 +1005,7 @@ let vo_magic_number = $VOMAGIC
 let state_magic_number = $STATEMAGIC
 let exec_extension = "$EXE"
 let with_geoproof = ref $with_geoproof
-let browser = "$ESCBROWSER"
+let browser = "$BROWSER"
 
 END_OF_COQ_CONFIG
 
@@ -983,32 +1032,32 @@ chmod a-w "$mlconfig_file"
 # Building the $COQTOP/config/Makefile file
 ###############################################
 
-rm -f "$COQSRC/config/Makefile"
+rm -f "$config_file"
 
 sed -e "s|LOCALINSTALLATION|$local|" \
-    -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
-    -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \
+    -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
+    -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \
     -e "s|COQSRCDIRECTORY|$COQSRC|" \
     -e "s|COQVERSION|$VERSION|" \
-    -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
-    -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
-    -e "s|BUILDLDPATH=|$ESCBUILDLDPATH|" \
-    -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
-    -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
-    -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
+    -e "s|BINDIRDIRECTORY|$BINDIR|" \
+    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
+    -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
+    -e "s|MANDIRDIRECTORY|$MANDIR|" \
+    -e "s|DOCDIRDIRECTORY|$DOCDIR|" \
+    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
     -e "s|EMACSCOMMAND|$EMACS|" \
-    -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \
+    -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
     -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
     -e "s|ARCHITECTURE|$ARCH|" \
     -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
     -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
-    -e "s|CAMLLIBDIRECTORY|$ESCCAMLLIB|" \
+    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
     -e "s|CAMLTAG|$CAMLTAG|" \
-    -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
+    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
     -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
     -e "s|CAMLP4TOOL|$camlp4oexec|" \
     -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
-    -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
+    -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \
     -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
     -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
     -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
@@ -1036,41 +1085,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
     -e "s|WITHDOCOPT|$with_doc|" \
     -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
-      "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"
-
-chmod a-w "$COQSRC/config/Makefile"
-
-##################################################
-# Building the $COQTOP/dev/ocamldebug-coq file
-##################################################
+      "$config_template" > "$config_file"
 
-OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
-
-if test "$coq_debug_flag" = "-g" ; then
-  rm -f $OCAMLDEBUGCOQ
-  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
-      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
-      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
-      $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
-  chmod a-w,a+x $OCAMLDEBUGCOQ
-fi
-
-####################################################
-# Fixing lablgtk types (before/after 2.6.0) 
-####################################################
-
-if [ ! "$COQIDE" = "no" ]; then 
-    if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
-       if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
-        cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
-       else
-	cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
-       fi
-    else
-	cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
-    fi
-fi  
+chmod a-w "$config_file"
 
 ##################################################
 # The end
diff --git a/coq.itarget b/coq.itarget
index 72684c23b..7488f421e 100644
--- a/coq.itarget
+++ b/coq.itarget
@@ -1,2 +1,3 @@
 binaries
-vo.otarget
+plugins/plugins.otarget
+theories/theories.otarget
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index a16a5e092..432e7ee51 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -21,68 +21,47 @@ open Scanf
 
 *)
 
+
 (** Generic file reader, which produces a list of strings, one per line *)
 
 let read_file f =
-  let ic = open_in f in
-  let lines = ref [] in
-  begin try
-    while true do lines := (input_line ic)::!lines done
-  with End_of_file -> () end;
-  close_in ic;
-  List.rev !lines
-
-(** Parse a config file such as config/Makefile. Valid lines are VAR=def.
-    If def is double-quoted we remove the "..." (first sscanf attempt with %S).
-    Otherwise, def is as long as possible (%s@\n prevents stopping at ' ').
-*)
-
-let read_env f =
-  let lines = read_file f in
-  let add, get = let l = ref [] in (fun x -> l:= x::!l), (fun () -> !l) in
-  let get_var_def s =
-    try sscanf s "%[A-Z0-9_]=%S" (fun v d -> add (v,d))
-    with _ ->
-      try sscanf s "%[A-Z0-9_]=%s@\n" (fun v d -> add (v,d))
-      with _ -> ()
-  in
-  List.iter get_var_def lines; get ()
+  let ic = open_in f and l = ref [] in
+  (try while true do l := (input_line ic)::!l done with End_of_file -> ());
+  close_in ic; List.rev !l
 
-let env_vars =
-  let f = "config/Makefile" in
-  try read_env f with _ -> (eprintf "Error while reading %s\n" f; exit 1)
 
-let get_env s =
-  try List.assoc s env_vars
-  with Not_found -> (eprintf "Unknown environment variable %s\n" s; exit 1)
+(** Configuration *)
 
+(** First, we access coq_config.ml indirectly : we symlink it to
+    myocamlbuild_config.ml, which is linked with this myocamlbuild.ml *)
 
+module Coq_config = struct include Myocamlbuild_config end
 
-(** Configuration *)
+let _ = begin
+  Options.ocamlc := A Coq_config.ocamlc;
+  Options.ocamlopt := A Coq_config.ocamlopt;
+  Options.ocamlmklib := A Coq_config.ocamlmklib;
+  Options.ocamldep := A Coq_config.ocamldep;
+  Options.ocamldoc := A Coq_config.ocamldoc;
+  Options.ocamlyacc := A Coq_config.ocamlyacc;
+  Options.ocamllex := A Coq_config.ocamllex;
+end
 
-let _ = Options.ocamlc := A(get_env "OCAMLC")
-let _ = Options.ocamlopt := A(get_env "OCAMLOPT")
-let _ = Options.ocamlmklib := A(get_env "OCAMLMKLIB")
-let _ = Options.ocamldep := A(get_env "OCAMLDEP")
-let _ = Options.ocamldoc := A(get_env "OCAMLDOC")
-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")
-let opt = (get_env "BEST" = "opt")
+let ocaml = A Coq_config.ocaml
+let camlp4o = A Coq_config.camlp4o
+let camlp4incl = S[A"-I"; A Coq_config.camlp4lib]
+let camlp4compat = Sh Coq_config.camlp4compat
+let opt = (Coq_config.best = "opt")
 let best_oext = if opt then ".native" else ".byte"
 let best_ext = if opt then ".opt" else ".byte"
-let hasdynlink = (get_env "HASNATDYNLINK" <> "false")
-let os5fix = (get_env "HASNATDYNLINK" = "os5fixme")
+let hasdynlink = Coq_config.has_natdynlink
+let os5fix = (Coq_config.natdynlinkflag = "os5fixme")
 let flag_dynlink = if hasdynlink then A"-DHasDynlink" else N
 let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no"
-let lablgtkincl = Sh(get_env "COQIDEINCLUDES")
-let local = (get_env "LOCAL" = "true")
-let coqsrc = get_env "COQSRC"
+let lablgtkincl = Sh Coq_config.coqideincl
+let local = Coq_config.local
+let coqsrc = Coq_config.coqsrc
+let cflags = S[A"-ccopt";A Coq_config.cflags]
 
 (** Do we want to inspect .ml generated from .ml4 ? *)
 let readable_genml = false
@@ -130,7 +109,22 @@ 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]
+let theoriesv =
+  let vo = string_list_of_file "theories/theories.itarget" in
+  List.map (fun s -> "theories/"^(Filename.chop_suffix s "o")) vo
+
+let contribv =
+  let vo = string_list_of_file "plugins/pluginsvo.itarget" in
+  List.map (fun s -> "plugins/"^(Filename.chop_suffix s "o")) vo
+
+let contribmllib =
+  let cma = string_list_of_file "plugins/pluginsbyte.itarget" in
+  List.map (fun s -> "plugins/"^(Filename.chop_suffix s ".cma")^".mllib") cma
+
+(** for correct execution of coqdep_boot, source files should have
+    been imported in _build (and NMake.v should have been created). *)
+
+let coqdepdeps = theoriesv @ contribv @ contribmllib
 
 let coqtop = "toplevel/coqtop"
 let coqide = "ide/coqide"
@@ -140,19 +134,22 @@ let coqmktop = "scripts/coqmktop"
 (** The list of binaries to build:
     (name of link in bin/, name in _build, install both or only best) *)
 
+type links = Both | Best | BestInPlace
+
 let all_binaries =
- [ "coqtop", coqtop, true;
-   "coqide", coqide, true;
-   "coqmktop", coqmktop, true;
-   "coqc", "scripts/coqc", true;
-   "coqchk", "checker/main", true;
-   "coqdep_boot", coqdepboot, false;
-   "coqdep", "tools/coqdep", false;
-   "coqdoc", "tools/coqdoc/main", false;
-   "coqwc", "tools/coqwc", false;
-   "coq_makefile", "tools/coq_makefile", false;
-   "coq-tex", "tools/coq_tex", false;
-   "gallina", "tools/gallina", false;
+ [ "coqtop", coqtop, Both;
+   "coqide", coqide, Both;
+   "coqmktop", coqmktop, Both;
+   "coqc", "scripts/coqc", Both;
+   "coqchk", "checker/main", Both;
+   "coqdep_boot", coqdepboot, Best;
+   "coqdep", "tools/coqdep", Best;
+   "coqdoc", "tools/coqdoc/main", Best;
+   "coqwc", "tools/coqwc", Best;
+   "coq_makefile", "tools/coq_makefile", Best;
+   "coq-tex", "tools/coq_tex", Best;
+   "gallina", "tools/gallina", Best;
+   "csdpcert", "plugins/micromega/csdpcert", BestInPlace;
  ]
 
 let coqtopbest = coqtop^best_oext
@@ -162,8 +159,8 @@ let coqmktopbest = coqmktop^best_oext
 let binaries_deps =
   let rec deps = function
     | [] -> []
-    | (_,bin,both) :: l ->
-	if opt && both then (bin^".native") :: (bin^".byte") :: deps l
+    | (_,bin,kind) :: l ->
+	if opt && kind=Both then (bin^".native") :: (bin^".byte") :: deps l
 	else (bin^best_oext) :: deps l
   in deps all_binaries
 
@@ -172,14 +169,17 @@ let ln_sf toward f =
 
 let rec make_bin_links = function
   | [] -> ()
-  | (b,ob,true) :: l ->
+  | (b,ob,Both) :: l ->
       ln_sf ("../"^ !_build^"/"^ob^".byte") ("bin/"^b^".byte");
       if opt then ln_sf ("../"^ !_build^"/"^ob^".native") ("bin/"^b^".opt");
       ln_sf (b^best_ext) ("bin/"^b);
       make_bin_links l
-  | (b,ob,false) :: l ->
+  | (b,ob,Best) :: l ->
       ln_sf ("../"^ !_build^"/"^ob^best_oext) ("bin/"^b);
       make_bin_links l
+  | (b,ob,BestInPlace) :: l ->
+      ln_sf (b^best_oext) ob;
+      make_bin_links l
 
 let incl f = Ocaml_utils.ocaml_include_flags f
 
@@ -189,14 +189,6 @@ let initial_actions () = begin
   make_bin_links all_binaries;
   (** We "pre-create" a few subdirs in _build to please coqtop *)
   Shell.mkdir_p (!_build^"/dev");
-  (** Moreover, we "pre-import" in _build the sources file that will be needed
-      by coqdep_boot *)
-  (*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")))
 end
 
 let extra_rules () = begin
@@ -275,7 +267,7 @@ let extra_rules () = begin
 (** C code for the VM *)
 
   dep ["compile"; "c"] c_headers;
-  flag ["compile"; "c"] (S[A"-ccopt";A"-fno-defer-pop -Wall -Wno-unused"]);
+  flag ["compile"; "c"] cflags;
   dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun];
 
 (** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *)
@@ -334,7 +326,9 @@ let extra_rules () = begin
 
 (** Coq files dependencies *)
 
-  rule ".v.d" ~prod:"%.v.depends" ~deps:(["%.v";coqdepbest]@genvfiles)
+  rule "coqdepready" ~stamp:"coqdepready" ~deps:coqdepdeps (fun _ _ -> Nop);
+
+  rule ".v.d" ~prod:"%.v.depends" ~deps:["%.v";coqdepbest;"coqdepready"]
     (fun env _ ->
        let v = env "%.v" and vd = env "%.v.depends" in
        (** NB: this relies on all .v files being already in _build. *)
diff --git a/plugins/plugins.itarget b/plugins/plugins.itarget
new file mode 100644
index 000000000..56aa42b06
--- /dev/null
+++ b/plugins/plugins.itarget
@@ -0,0 +1,3 @@
+pluginsopt.otarget
+pluginsbyte.otarget
+pluginsvo.otarget
\ No newline at end of file
diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
new file mode 100644
index 000000000..7e0a77787
--- /dev/null
+++ b/plugins/pluginsbyte.itarget
@@ -0,0 +1,25 @@
+field/field_plugin.cma
+setoid_ring/newring_plugin.cma
+extraction/extraction_plugin.cma
+firstorder/ground_plugin.cma
+rtauto/rtauto_plugin.cma
+interface/coqinterface_plugin.cma
+interface/coqparser_plugin.cma
+fourier/fourier_plugin.cma
+romega/romega_plugin.cma
+omega/omega_plugin.cma
+micromega/micromega_plugin.cma
+dp/dp_plugin.cma
+xml/xml_plugin.cma
+subtac/subtac_plugin.cma
+ring/ring_plugin.cma
+cc/cc_plugin.cma
+groebner/groebner_plugin.cma
+funind/recdef_plugin.cma
+syntax/ascii_syntax_plugin.cma
+syntax/nat_syntax_plugin.cma
+syntax/numbers_syntax_plugin.cma
+syntax/r_syntax_plugin.cma
+syntax/string_syntax_plugin.cma
+syntax/z_syntax_plugin.cma
+quote/quote_plugin.cma
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
new file mode 100644
index 000000000..e8e7868b7
--- /dev/null
+++ b/plugins/pluginsopt.itarget
@@ -0,0 +1,25 @@
+field/field_plugin.cmxa
+setoid_ring/newring_plugin.cmxa
+extraction/extraction_plugin.cmxa
+firstorder/ground_plugin.cmxa
+rtauto/rtauto_plugin.cmxa
+interface/coqinterface_plugin.cmxa
+interface/coqparser_plugin.cmxa
+fourier/fourier_plugin.cmxa
+romega/romega_plugin.cmxa
+omega/omega_plugin.cmxa
+micromega/micromega_plugin.cmxa
+dp/dp_plugin.cmxa
+xml/xml_plugin.cmxa
+subtac/subtac_plugin.cmxa
+ring/ring_plugin.cmxa
+cc/cc_plugin.cmxa
+groebner/groebner_plugin.cmxa
+funind/recdef_plugin.cmxa
+syntax/ascii_syntax_plugin.cmxa
+syntax/nat_syntax_plugin.cmxa
+syntax/numbers_syntax_plugin.cmxa
+syntax/r_syntax_plugin.cmxa
+syntax/string_syntax_plugin.cmxa
+syntax/z_syntax_plugin.cmxa
+quote/quote_plugin.cmxa
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
new file mode 100644
index 000000000..af4d23310
--- /dev/null
+++ b/plugins/pluginsvo.itarget
@@ -0,0 +1,60 @@
+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
+interface/CoqInterface.vo
+#interface/CoqParser.vo  (should not be compiled)
+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
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
diff --git a/vo.itarget b/vo.itarget
deleted file mode 100644
index 8898dd8fa..000000000
--- a/vo.itarget
+++ /dev/null
@@ -1,407 +0,0 @@
-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  (extraction of micromega.ml)
-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