diff options
| -rw-r--r-- | tools/coqdep.ml | 4 | ||||
| -rw-r--r-- | tools/coqdep_boot.ml | 2 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 27 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 1 |
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 |