Revert "Merge remote-tracking branch 'github/pr/229' into trunk"

This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.

Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.

14 files changed, 105 insertions, 280 deletions

diff --git a/INSTALL b/INSTALL
index 56ff522dc..5a300010d 100644
--- a/INSTALL
+++ b/INSTALL
@@ -55,6 +55,8 @@ QUICK INSTALLATION PROCEDURE.
 1. ./configure
 2. make
 3. make install (you may need superuser rights)
+4. make clean
+
 
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
@@ -130,13 +132,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 
 	make
 
-   to compile Coq in the best OCaml mode available (native-code if supported,
-   bytecode otherwise).
+   to compile Coq in Objective Caml bytecode (and native-code if supported).
 
    This will compile the entire system. This phase can take more or less time,
-   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.
+   depending on your architecture and is fairly verbose.
 
 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
@@ -152,19 +151,7 @@ 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- 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.)
+7- You can now clean all the sources. (You can even erase them.)
 
 	make clean
 
@@ -202,14 +189,11 @@ THE AVAILABLE COMMANDS.
 	coqtop		The Coq toplevel
 	coqc		The Coq compiler
 
-   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.
+   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.
 
     * `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 db23ad0a8..93b89a489 100644
--- a/Makefile
+++ b/Makefile
@@ -109,17 +109,14 @@ 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 "Bytecode compilation is now a separate target:"
-	@echo "   make byte"
-	@echo "   make install-byte"
-	@echo "Please do 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 90834ec8c..ebf2996f1 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -17,16 +17,9 @@
 
 world: coq coqide documentation revision
 
-coq: coqlib coqbinaries tools
+coq: coqlib coqbinaries tools printers
 
-# 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
+.PHONY: world coq
 
 ###########################################################################
 # Includes
@@ -91,7 +84,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
-BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
+BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
 # or only abbreviated versions. 
@@ -181,7 +174,7 @@ ifndef ORDER_ONLY_SEP
 $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.))
 endif
 
-VO_TOOLS_DEP := $(COQTOPBEST)
+VO_TOOLS_DEP := $(COQTOPEXE)
 ifdef COQ_XML
  VO_TOOLS_DEP += $(COQDOC)
 endif
@@ -320,11 +313,11 @@ grammar/%.cmi: grammar/%.mli
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-.PHONY: coqbinaries coqbyte
+.PHONY: coqbinaries
 
-coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \
+ $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE)
 
-coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
@@ -510,13 +503,18 @@ test-suite: world $(ALLSTDLIB).v
 
 # 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
+%.cmx: %.mlpack %.cmo
 	$(SHOW)'OCAMLOPT -pack -o $@'
-	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^)
 
 COND_BYTEFLAGS= \
  $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS)
@@ -532,6 +530,27 @@ 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:
@@ -542,11 +561,11 @@ plugins/micromega/csdpcert_FORPACK:=
 
 plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $($(@:.cmx=_FORPACK)) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
 
 %.cmx: %.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
 
 %.cmxs: %.cmx
 	$(SHOW)'OCAMLOPT -shared -o $@'
@@ -631,7 +650,7 @@ endif
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
 
 ###########################################################################
 
diff --git a/Makefile.checker b/Makefile.checker
index 435d8e8f6..3ea0baced 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) -c $<
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $<
 
 md5chk:
 	$(SHOW)'MD5SUM cic.mli'
diff --git a/Makefile.common b/Makefile.common
index aacd801b5..49fe1fd93 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -41,26 +41,10 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 # Object and Source files
 ###########################################################################
 
-ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
- # static link of plugins, do not mention them in .v.d
- DYNDEP:=-dyndep no
-else
- DYNDEP:=-dyndep var
-endif
-
-# Which coqtop do we use to build .vo file ? The best ;-)
-# Note: $(BEST) could be overridden by the user if a byte build is desired
-# Note: coqdep -dyndep var will use $(DYNOBJ) and $(DYNLIB) extensions
-# for Declare ML Module files.
-
-ifeq ($(BEST),opt)
-COQTOPBEST:=$(COQTOPEXE)
-DYNOBJ:=.cmxs
-DYNLIB:=.cmxs
+ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
+  DEPNATDYN:=
 else
-COQTOPBEST:=$(COQTOPBYTE)
-DYNOBJ:=.cmo
-DYNLIB:=.cma
+  DEPNATDYN:=-natdynlink no
 endif
 
 INSTALLBIN:=install
diff --git a/Makefile.ide b/Makefile.ide
index 0cfbdeb4e..48a269ab7 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -61,30 +61,23 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
 # CoqIde special targets
 ###########################################################################
 
-.PHONY: coqide coqide-opt coqide-byte coqide-files
-.PHONY: ide-toploop ide-byteloop ide-optloop
+.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
+.PHONY: ide-toploop
 
 # target to build CoqIde
-coqide: coqide-files coqide-opt theories/Init/Prelude.vo
+coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
 
-ifeq ($(HASCOQIDE),opt)
-coqide-opt: $(COQIDE) ide-toploop
-else
-coqide-opt: ide-toploop
-endif
-
-ifeq ($(HASCOQIDE),no)
-coqide-byte: ide-byteloop
+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)
 else
-coqide-byte: $(COQIDEBYTE) ide-byteloop
+ide-toploop: $(IDETOPLOOPCMA)
 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 $@'
@@ -116,14 +109,14 @@ ide/%.cmo: ide/%.ml
 
 ide/%.cmx: ide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $<
 
 
 ####################
 ## Install targets
 ####################
 
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 
 ifeq ($(HASCOQIDE),no)
 install-coqide: install-ide-toploop
@@ -131,26 +124,20 @@ 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) \
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
 	  $(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 b4aad7bdd..4dad8cf0d 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -61,26 +61,15 @@ 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) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(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)
@@ -104,7 +93,7 @@ install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
+	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
 ifeq ($(BEST),opt)
 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
@@ -112,8 +101,11 @@ endif
 
 install-library:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES)
+	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
+ifndef CUSTOM
+	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
+endif
 ifeq ($(BEST),opt)
 	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
 	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli
deleted file mode 100644
index 57c4e50ca..000000000
--- a/plugins/micromega/sos_types.mli
+++ /dev/null
@@ -1,40 +0,0 @@
-(************************************************************************)
-(*  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/coq_makefile.ml b/tools/coq_makefile.ml
index f116c5580..c86253477 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -293,8 +293,9 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
     let cmxss = List.rev_append cmos mllibs in
     let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in
     let where_what_oth = vars_to_put_by_root
-      [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);
-       ("NATIVEFILES",vfiles);("CMIFILES",cmis)]
+      [("VOFILES",vfiles);("VFILES",vfiles);
+       ("GLOBFILES",vfiles);("NATIVEFILES",vfiles);
+       ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)]
       inc in
     let doc_dir = where_put_doc inc in
     if is_install = Project_file.UnspecInstall then begin
@@ -306,12 +307,6 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
       print "\n";
     end;
     if not_empty cmxss then begin
-      print "install-byte:\n";
-      install_include_by_root "0755"
-        (vars_to_put_by_root [("CMOFILES",cmos);("CMAFILES",mllibs)] inc);
-      print "\n";
-    end;
-    if not_empty cmxss then begin
       print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
       printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
       printf "\t install -m 0755 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
@@ -511,7 +506,7 @@ let variables is_install opt (args,defs) =
     end;
     (* Coq executables and relative variables *)
     if !some_vfile || !some_mlpackfile || !some_mllibfile then
-      print "COQDEP?=\"$(COQBIN)coqdep\" -c -dyndep var\n";
+      print "COQDEP?=\"$(COQBIN)coqdep\" -c\n";
     if !some_vfile then begin
     print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
     print "COQCHKFLAGS?=-silent -o\n";
@@ -542,16 +537,7 @@ else
 CAMLP4EXTEND=
 endif\n";
     print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\
-  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n";
-    print "ifeq '$(OPT)' '-byte'\n";
-    print "USEBYTE:=true\n";
-    print "DYNOBJ:=.cmo\n";
-    print "DYNLIB:=.cma\n";
-    print "else\n";
-    print "USEBYTE:=\n";
-    print "DYNOBJ:=.cmxs\n";
-    print "DYNLIB:=.cmxs\n";
-    print "endif\n\n";
+  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
     end;
     match is_install with
       | Project_file.NoInstall -> ()
@@ -770,19 +756,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
   print "HASNATDYNLINK_OR_EMPTY :=\n";
   print "endif\n\n";
   section "Definition of the toplevel targets.";
-  let has_cmo = !some_mlfile || !some_ml4file || !some_mlpackfile in
-  let has_ml = has_cmo || !some_mllibfile in
-  print "all:";
-  if !some_vfile then print " $(VOFILES)";
-  if has_ml then print " $(if $(USEBYTE),bytefiles,optfiles)";
+  print "all: ";
+  if !some_vfile then print "$(VOFILES) ";
+  if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) ";
+  if !some_mllibfile then print "$(CMAFILES) ";
+  if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile
+  then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) ";
   print_list "\\\n  " other_targets; print "\n\n";
-  print "bytefiles:";
-  if has_cmo then print " $(CMOFILES)";
-  if !some_mllibfile then print " $(CMAFILES)";
-  print "\n\n";
-  print "optfiles:";
-  if has_ml then print " $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES))";
-  print "\n\n";
   if !some_mlifile then
     begin
       print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
@@ -828,11 +808,9 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
   print ".PHONY: ";
   print_list
     " "
-    ("all" :: "archclean" :: "beautify" :: "byte" :: "bytefiles"
-     :: "clean" :: "cleanall"
-     :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-byte"
-     :: "install-doc" :: "install-natdynlink" :: "install-toploop"
-     :: "opt" :: "optfiles" :: "printenv"
+    ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall"
+     :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc"
+     :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv"
      :: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo"
      :: (sds@(CList.map_filter
 		(fun (n,_,is_phony,_) ->
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 991a3221f..a7c32e1d6 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -320,25 +320,19 @@ 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 = 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)"]
+          let base = file_name s dir in
+          let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in
+          (escape base, suff ^ opt)
         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
@@ -455,7 +449,6 @@ 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 "."))
@@ -483,22 +476,17 @@ 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 25f62d2be..6fc826833 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -16,11 +16,7 @@ open Coqdep_common
 *)
 
 let rec parse = function
-  | "-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
+  | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; 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 8bf7fee4b..cc63c13d7 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_dynlink] below).
+    options (see for instance [option_natdynlk] below).
 *)
 
 module StrSet = Set.Make(String)
@@ -26,11 +26,9 @@ 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_dynlink = ref Both
+let option_natdynlk = ref true
 let option_boot = ref false
 let option_mldep = ref None
 
@@ -382,16 +380,10 @@ let rec traite_fichier_Coq suffixe verbose f =
        		end) strl
 	  | Declare sl ->
 	      let declare suff dir s =
-		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 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 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 205e99176..633c474ad 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -19,10 +19,7 @@ val find_dir_logpath: string -> string list
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
-
-type dynlink = Opt | Byte | Both | No | Variable
-
-val option_dynlink : dynlink ref
+val option_natdynlk : bool 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
deleted file mode 100644
index 2c9b3fb8e..000000000
--- a/tools/coqdoc/cdglobals.mli
+++ /dev/null
@@ -1,49 +0,0 @@
-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