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.

6 files changed, 28 insertions, 126 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index f116c5580d..c86253477b 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 991a3221f4..a7c32e1d65 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 25f62d2bec..6fc826833e 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 8bf7fee4bd..cc63c13d7b 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 205e99176c..633c474ada 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 2c9b3fb8e8..0000000000
--- 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