[coqdep] Remove deprecated -slash , unused, undocumented -mldep option.

4 files changed, 1 insertions, 33 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index fcafd826f0..8a994b99c7 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -20,7 +20,6 @@ open Minisys
 
     As of today, this module depends on the following Coq modules:
 
-    - Flags
     - Envars
     - CoqProject_file
 
@@ -126,9 +125,6 @@ let rec parse = function
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
-  | "-slash" :: ll ->
-    coqdep_warning "warning: option -slash has no effect and is deprecated.";
-    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
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 1730dd3d68..257d4cc0fd 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -28,8 +28,6 @@ let rec parse = function
   | "-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 ->
-      option_mldep := Some ocamldep; option_c := true; parse ll
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 775c528176..bd72a52adf 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -35,7 +35,6 @@ let option_c = ref false
 let option_noglob = ref false
 let option_dynlink = ref Both
 let option_boot = ref false
-let option_mldep = ref None
 
 let norec_dirs = ref StrSet.empty
 
@@ -246,26 +245,7 @@ let depend_ML str =
         (" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
-let soustraite_fichier_ML dep md ext =
-  try
-    let chan = open_process_in (dep^" -modules "^md^ext) in
-    let list = ocamldep_parse (Lexing.from_channel chan) in
-    let a_faire = ref "" in
-    let a_faire_opt = ref "" in
-    List.iter
-      (fun str ->
-         let byte,opt = depend_ML str in
-         a_faire := !a_faire ^ byte;
-         a_faire_opt := !a_faire_opt ^ opt)
-      (List.rev list);
-    (!a_faire, !a_faire_opt)
-  with
-    | Sys_error _ -> ("","")
-    | _ ->
-       Printf.eprintf "Coqdep: subprocess %s failed on file %s%s\n" dep md ext;
-       exit 1
-
-let autotraite_fichier_ML md ext =
+let traite_fichier_ML md ext =
   try
     let chan = open_in (md ^ ext) in
     let buf = Lexing.from_channel chan in
@@ -290,11 +270,6 @@ let autotraite_fichier_ML md ext =
     (!a_faire, !a_faire_opt)
   with Sys_error _ -> ("","")
 
-let traite_fichier_ML md ext =
-  match !option_mldep with
-    | Some dep -> soustraite_fichier_ML dep md ext
-    | None -> autotraite_fichier_ML md ext
-
 let traite_fichier_modules md ext =
   try
     let chan = open_in (md ^ ext) in
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 6d49f7e06c..96266b8e36 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -30,7 +30,6 @@ val write_vos : 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
 type dir = string option