Makefile: no bytecode compilation in make world, see make byte instead

 On a machine for which ocamlopt is available, the make world will now
 perform bytecode compilation only in grammar/ (up to the syntax
 extension grammar.cma), and then exclusively use ocamlopt.
 In particular, make world do not build bin/coqtop.byte.
 A separate rule 'make byte' does it, as well as bytecode plugins and
 things like dev/printers.cma.

 'make install' deals only with the part built by 'make', while a new
 rule 'make install-byte' installs the part built by 'make byte'.

 IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any
 parallel mix of native and byte rules. These are known to crash sometimes,
 see below. Instead, do rather 'make -j && make -j byte'.

 Indeed, apart from marginal compilation speed-up for users not interested
 in byte versions, the main reason for this commit is to discourage any
 simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and
 ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli,
 and in case of parallel build this may happen at the very moment another
 ocaml(c|opt) is accessing this .cmi. Until now, this issue has been
 handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in
 Makefile.build). But these hacks weren't obvious to extend to ocamlopt
 -pack vs. ocamlopt -pack.

 coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML
 Module influences the .v.d dependency file. Possible values are:
 -dyndep opt : regular situation now, depends only on .cmxs
 -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a)
 -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs
 -dyndep none : interesting for coqtop with statically linked plugins
 -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d
   instead of extensions .cm*, so that the choice is made in the rest of the
   makefile (see a future commit about coq_makefile)

 NB: two extra mli added to avoid building unecessary .cmo during 'make world',
 without having to use the ocamldep -native option.

 NB: we should state somewhere that coqmktop -top won't work unless
  'make byte' was done first

13 files changed, 228 insertions, 87 deletions

diff --git a/INSTALL b/INSTALL
index eacbec299..39fb1849a 100644
--- a/INSTALL
+++ b/INSTALL
@@ -55,8 +55,6 @@ QUICK INSTALLATION PROCEDURE.
 1. ./configure
 2. make
 3. make install (you may need superuser rights)
-4. make clean
-
 
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
@@ -131,10 +129,13 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 
 	make
 
-   to compile Coq in Objective Caml bytecode (and native-code if supported).
+   to compile Coq in the best OCaml mode available (native-code if supported,
+   bytecode otherwise).
 
    This will compile the entire system. This phase can take more or less time,
-   depending on your architecture and is fairly verbose.
+   depending on your architecture and is fairly verbose. On a multi-core machine,
+   it is recommended to compile in parallel, via make -jN where N is your number
+   of cores.
 
 6- You can now install the Coq system. Executables, libraries, manual pages
    and emacs mode are copied in some standard places of your system, defined at
@@ -150,7 +151,19 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
         (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
         (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
 
-7- You can now clean all the sources. (You can even erase them.)
+7- Optionally, you could build the bytecode version of Coq via:
+
+        make byte
+
+   and install it via
+
+        make install-byte
+
+  This version is quite slower than the native code version of Coq, but could
+  be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
+  toplevel accessible via the Drop command.
+
+8- You can now clean all the sources. (You can even erase them.)
 
 	make clean
 
@@ -182,11 +195,14 @@ THE AVAILABLE COMMANDS.
 	coqtop		The Coq toplevel
 	coqc		The Coq compiler
 
-   Under architecture where ocamlopt is available, there are actually two
-   binaries for the interactive system, coqtop.byte and coqtop (respectively
-   bytecode and native code versions of Coq).  coqtop is a link to coqtop.byte
-   otherwise. coqc also invokes the fastest version of Coq.  Options -opt and
-   -byte to coqtop and coqc selects a particular binary.
+   Under architecture where ocamlopt is available, coqtop is the native code
+   version of Coq. On such architecture, you could additionally request
+   the build of the bytecode version of Coq via 'make byte' and install it via
+   'make install-byte'. This will create  an extra binary named coqtop.byte,
+   that could be used for debugging purpose. If native code isn't available,
+   coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
+   coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
+   and coqc selects a particular binary.
 
     * `coqtop' launches Coq in the interactive mode. By default it loads
       basic logical definitions and tactics from the Init directory.
diff --git a/Makefile b/Makefile
index d1fa99ccb..23c6ea638 100644
--- a/Makefile
+++ b/Makefile
@@ -116,16 +116,19 @@ NOARG: world
 .PHONY: NOARG help noconfig submake
 
 help:
-	@echo "Please use either"
+	@echo "Please use either:"
 	@echo "   ./configure"
 	@echo "   make world"
 	@echo "   make install"
 	@echo "   make clean"
 	@echo "or make archclean"
-	@echo
 	@echo "For make to be verbose, add VERBOSE=1"
-	@echo
 	@echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1"
+	@echo
+	@echo "Bytecode compilation is now a separate target:"
+	@echo "   make byte"
+	@echo "   make install-byte"
+	@echo "Please do not mix bytecode and native targets in the same make -j"
 
 UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
 ifdef UNSAVED_FILES
diff --git a/Makefile.build b/Makefile.build
index 8aedd9cec..e3a74aaee 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -51,9 +51,16 @@ COQ_XML ?=
 
 world: coq coqide documentation revision
 
-coq: coqlib coqbinaries tools printers
+coq: coqlib coqbinaries tools
 
-.PHONY: world coq
+# Note: 'world' do not build the bytecode binaries anymore.
+# For that, you can use the 'byte' rule. Native and byte compilations
+# shouldn't be done in a same make -j... run, otherwise both ocamlc and
+# ocamlopt might race for access to the same .cmi files.
+
+byte: coqbyte coqide-byte pluginsbyte printers
+
+.PHONY: world coq byte
 
 ###########################################################################
 # Includes
@@ -290,11 +297,11 @@ grammar/%.cmi: grammar/%.mli
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-.PHONY: coqbinaries
+.PHONY: coqbinaries coqbyte
 
-coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \
- $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
 
+coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
@@ -486,18 +493,13 @@ kernel/kernel.cma: kernel/kernel.mllib
 
 # For plugin packs
 
-# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's
-# apparently no way to avoid that (no -intf-suffix hack as below).
-# We at least ensure that these two commands won't run at the same time, by a fake
-# dependency from the packed .cmx to the packed .cmo.
-
 %.cmo: %.mlpack
 	$(SHOW)'OCAMLC -pack -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
-%.cmx: %.mlpack %.cmo
+%.cmx: %.mlpack
 	$(SHOW)'OCAMLOPT -pack -o $@'
-	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^)
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
 COND_BYTEFLAGS= \
  $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS)
@@ -513,27 +515,6 @@ COND_OPTFLAGS= \
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
 
-## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around.
-## This can lead to nasty things with make -j. To avoid that:
-##  1) We make .cmx always depend on .cmi
-##  2) This .cmi will be created from the .mli, or trigger the compilation of the
-##    .cmo if there's no .mli (see rule below about MLWITHOUTMLI)
-##  3) We tell ocamlopt to use the .cmi as the interface source file. With this
-##     hack, everything goes as if there is a .mli, and the .cmi is preserved
-##     and the .cmx is checked with respect to this .cmi
-
-HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi)
-
-define diff
- $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
-endef
-
-MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
-
-$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi  # for .ml with .mli this is already the case
-
-$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo
-
 # NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep
 # The only exceptions are the sources of the csdpcert binary.
 # To avoid warnings, we set them manually here:
@@ -544,11 +525,11 @@ plugins/micromega/csdpcert_FORPACK:=
 
 plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $($(@:.cmx=_FORPACK)) -c $<
 
 %.cmx: %.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c $<
 
 %.cmxs: %.cmx
 	$(SHOW)'OCAMLOPT -shared -o $@'
@@ -633,7 +614,7 @@ endif
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET)
 
 ###########################################################################
 
diff --git a/Makefile.checker b/Makefile.checker
index 3ea0baced..435d8e8f6 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -71,7 +71,7 @@ checker/%.cmo: checker/%.ml
 
 checker/%.cmx: checker/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $<
 
 md5chk:
 	$(SHOW)'MD5SUM cic.mli'
diff --git a/Makefile.common b/Makefile.common
index d5f79d76b..3d4e7829a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -41,10 +41,11 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 # Object and Source files
 ###########################################################################
 
-ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
-  DEPNATDYN:=
+ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
+ # static link of plugins, do not mention them in .v.d
+ DYNDEP:=-dyndep no
 else
-  DEPNATDYN:=-natdynlink no
+ DYNDEP:=-dyndep $(BEST)
 endif
 
 INSTALLBIN:=install
diff --git a/Makefile.ide b/Makefile.ide
index 48a269ab7..0cfbdeb4e 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -61,23 +61,30 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
 # CoqIde special targets
 ###########################################################################
 
-.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
-.PHONY: ide-toploop
+.PHONY: coqide coqide-opt coqide-byte coqide-files
+.PHONY: ide-toploop ide-byteloop ide-optloop
 
 # target to build CoqIde
-coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
+coqide: coqide-files coqide-opt theories/Init/Prelude.vo
 
-coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
-coqide-no:
-coqide-byte: $(COQIDEBYTE) $(COQIDE)
-coqide-opt:  $(COQIDEBYTE) $(COQIDE)
-coqide-files: $(IDEFILES)
-ifeq ($(BEST),opt)
-ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
+ifeq ($(HASCOQIDE),opt)
+coqide-opt: $(COQIDE) ide-toploop
 else
-ide-toploop: $(IDETOPLOOPCMA)
+coqide-opt: ide-toploop
 endif
 
+ifeq ($(HASCOQIDE),no)
+coqide-byte: ide-byteloop
+else
+coqide-byte: $(COQIDEBYTE) ide-byteloop
+endif
+
+coqide-files: $(IDEFILES)
+
+ide-byteloop: $(IDETOPLOOPCMA)
+ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs)
+ide-toploop: ide-$(BEST)loop
+
 ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
@@ -109,14 +116,14 @@ ide/%.cmo: ide/%.ml
 
 ide/%.cmx: ide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
 
 
 ####################
 ## Install targets
 ####################
 
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte
 
 ifeq ($(HASCOQIDE),no)
 install-coqide: install-ide-toploop
@@ -124,20 +131,26 @@ else
 install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 endif
 
+# Apparently, coqide.byte is not meant to be installed
+
+install-ide-byte:
+	$(MKDIR) $(FULLCOQLIB)
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA)
+	$(MKDIR) $(FULLCOQLIB)/toploop
+	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
+
 install-ide-bin:
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
 
 install-ide-toploop:
-	$(MKDIR) $(FULLCOQLIB)/toploop
-	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
 ifeq ($(BEST),opt)
 	$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
 endif
 
 install-ide-devfiles:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
+	$(INSTALLSH) $(FULLCOQLIB) \
 	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
 ifeq ($(BEST),opt)
 	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
diff --git a/Makefile.install b/Makefile.install
index 33f881c11..4a3227620 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -62,15 +62,26 @@ endif
 
 install-coq: install-binaries install-library install-coq-info install-devfiles
 
+ifeq ($(BEST),byte)
+install-coq: install-byte
+endif
+
 install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)/toploop
-	$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
 ifeq ($(BEST),opt)
 	$(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
 endif
 
+install-byte: install-ide-byte
+	$(MKDIR) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR)
+	$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
+	$(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS)
+ifndef CUSTOM
+	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
+endif
 
 install-tools:
 	$(MKDIR) $(FULLBINDIR)
@@ -94,7 +105,7 @@ install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
+	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
 	$(INSTALLSH)  $(FULLCOQLIB) tools/CoqMakefile.in
 ifeq ($(BEST),opt)
@@ -103,7 +114,7 @@ endif
 
 install-library:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
+	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES)
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
 	$(MKDIR) $(FULLCOQLIB)/kernel/byterun
 ifndef CUSTOM
diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli
new file mode 100644
index 000000000..57c4e50ca
--- /dev/null
+++ b/plugins/micromega/sos_types.mli
@@ -0,0 +1,40 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* The type of positivstellensatz -- used to communicate with sos *)
+
+type vname = string;;
+
+type term =
+| Zero
+| Const of Num.num
+| Var of vname
+| Inv of term
+| Opp of term
+| Add of (term * term)
+| Sub of (term * term)
+| Mul of (term * term)
+| Div of (term * term)
+| Pow of (term * int);;
+
+val output_term : out_channel -> term -> unit
+
+type positivstellensatz =
+   Axiom_eq of int
+ | Axiom_le of int
+ | Axiom_lt of int
+ | Rational_eq of Num.num
+ | Rational_le of Num.num
+ | Rational_lt of Num.num
+ | Square of term
+ | Monoid of int list
+ | Eqmul of term * positivstellensatz
+ | Sum of positivstellensatz * positivstellensatz
+ | Product of positivstellensatz * positivstellensatz;;
+
+val output_psatz : out_channel -> positivstellensatz -> unit
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 044399544..cba9c3eb0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -320,19 +320,25 @@ let treat_coq_file chan =
         List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
       | Declare sl ->
         let declare suff dir s =
-          let base = file_name s dir in
-          let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in
-          (escape base, suff ^ opt)
+          let base = escape (file_name s dir) in
+          match !option_dynlink with
+          | No -> []
+          | Byte -> [base,suff]
+          | Opt -> [base,".cmxs"]
+          | Both -> [base,suff; base,".cmxs"]
+          | Variable ->
+             if suff=".cmo" then [base,"$(DYNOBJ)"]
+             else [base,"$(DYNLIB)"]
         in
         let decl acc str =
           let s = basename_noext str in
           if not (StrSet.mem s !deja_vu_ml) then
             let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
             match search_mllib_known s with
-            | Some mldir -> (declare ".cma" mldir s) :: acc
+            | Some mldir -> (declare ".cma" mldir s) @ acc
             | None ->
               match search_ml_known s with
-              | Some mldir -> (declare ".cmo" mldir s) :: acc
+              | Some mldir -> (declare ".cmo" mldir s) @ acc
               | None -> acc
           else acc
         in
@@ -449,6 +455,7 @@ let usage () =
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -suffix s : \n";
   eprintf "  -slash : deprecated, no effect\n";
+  eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed";
   exit 1
 
 let split_period = Str.split (Str.regexp (Str.quote "."))
@@ -476,17 +483,22 @@ let rec parse = function
   | "-slash" :: ll ->
     Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
     parse ll
+  | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+  | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+  | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+  | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+  | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | ("-h"|"--help"|"-help") :: _ -> usage ()
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
+  if not Coq_config.has_natdynlink then option_dynlink := No;
   parse (List.tl (Array.to_list Sys.argv));
   (* Add current dir with empty logical path if not set by options above. *)
   (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd()))
    with Not_found -> add_norec_dir_import add_known "." []);
-  if not Coq_config.has_natdynlink then option_natdynlk := false;
   (* NOTE: These directories are searched from last to first *)
   if !option_boot then begin
     add_rec_dir_import add_known "theories" ["Coq"];
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 6fc826833..25f62d2be 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -16,7 +16,11 @@ open Coqdep_common
 *)
 
 let rec parse = function
-  | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
+  | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+  | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+  | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+  | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+  | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
   | "-mldep" :: ocamldep :: ll ->
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index f5e93527c..bf8bcd0c4 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -15,7 +15,7 @@ open Minisys
     behavior is the one of [coqdep -boot]. Its only dependencies
     are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so.
     If it need someday some additional information, pass it via
-    options (see for instance [option_natdynlk] below).
+    options (see for instance [option_dynlink] below).
 *)
 
 module StrSet = Set.Make(String)
@@ -26,9 +26,11 @@ module StrListMap = Map.Make(StrList)
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
+type dynlink = Opt | Byte | Both | No | Variable
+
 let option_c = ref false
 let option_noglob = ref false
-let option_natdynlk = ref true
+let option_dynlink = ref Both
 let option_boot = ref false
 let option_mldep = ref None
 
@@ -383,10 +385,16 @@ let rec traite_fichier_Coq suffixe verbose f =
        		end) strl
 	  | Declare sl ->
 	      let declare suff dir s =
-		let base = file_name s dir in
-		let opt = if !option_natdynlk then " "^base^".cmxs" else "" in
-		printf " %s%s%s" (escape base) suff opt
-	      in
+		let base = escape (file_name s dir) in
+                match !option_dynlink with
+                | No -> ()
+                | Byte -> printf " %s%s" base suff
+                | Opt -> printf " %s.cmxs" base
+                | Both -> printf " %s%s %s.cmxs" base suff base
+                | Variable ->
+                   printf " %s%s" base
+                    (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")
+              in
 	      let decl str =
                 let s = basename_noext str in
 		if not (StrSet.mem s !deja_vu_ml) then begin
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 10da0240d..8c1787d31 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -19,7 +19,10 @@ val find_dir_logpath: string -> string list
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
-val option_natdynlk : bool ref
+
+type dynlink = Opt | Byte | Both | No | Variable
+
+val option_dynlink : dynlink ref
 val option_mldep : string option ref
 val norec_dirs : StrSet.t ref
 val suffixe : string ref
diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli
new file mode 100644
index 000000000..2c9b3fb8e
--- /dev/null
+++ b/tools/coqdoc/cdglobals.mli
@@ -0,0 +1,49 @@
+type target_language = LaTeX | HTML | TeXmacs | Raw
+val target_language : target_language ref
+type output_t = StdOut | MultFiles | File of string
+val output_dir : string ref
+val out_to : output_t ref
+val out_channel : out_channel ref
+val ( / ) : string -> string -> string
+val coqdoc_out : string -> string
+val open_out_file : string -> unit
+val close_out_file : unit -> unit
+type glob_source_t = NoGlob | DotGlob | GlobFile of string
+val glob_source : glob_source_t ref
+val normalize_path : string -> string
+val normalize_filename : string -> string * string
+val guess_coqlib : unit -> string
+val header_trailer : bool ref
+val header_file : string ref
+val header_file_spec : bool ref
+val footer_file : string ref
+val footer_file_spec : bool ref
+val quiet : bool ref
+val light : bool ref
+val gallina : bool ref
+val short : bool ref
+val index : bool ref
+val multi_index : bool ref
+val index_name : string ref
+val toc : bool ref
+val page_title : string ref
+val title : string ref
+val externals : bool ref
+val coqlib : string ref
+val coqlib_path : string ref
+val raw_comments : bool ref
+val parse_comments : bool ref
+val plain_comments : bool ref
+val toc_depth : int option ref
+val lib_name : string ref
+val lib_subtitles : bool ref
+val interpolate : bool ref
+val inline_notmono : bool ref
+val charset : string ref
+val inputenc : string ref
+val latin1 : bool ref
+val utf8 : bool ref
+val set_latin1 : unit -> unit
+val set_utf8 : unit -> unit
+type coq_module = string
+type file = Vernac_file of string * coq_module | Latex_file of string