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.

1 files changed, 6 insertions, 18 deletions

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"];