[coqdep] mli cleanup, remove unused functions

3 files changed, 40 insertions, 68 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 745cf950b5..950c784325 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -9,9 +9,8 @@
 (************************************************************************)
 
 open Format
-open Coqdep_lexer
-open Coqdep_common
 open Minisys
+open Coqdep_common
 
 (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
     are now in [Coqdep_common]. The code that remains here concerns
@@ -29,47 +28,6 @@ open Minisys
 
 let option_sort = ref false
 
-let warning_mult suf iter =
-  let tab = Hashtbl.create 151 in
-  let check f d =
-    begin try
-      let d' = Hashtbl.find tab f in
-      if (Filename.dirname (file_name f d))
-        <> (Filename.dirname (file_name f d')) then begin
-          coqdep_warning "the file %s is defined twice!" (f ^ suf)
-        end
-    with Not_found -> () end;
-    Hashtbl.add tab f d
-  in
-  iter check
-
-let sort () =
-  let seen = Hashtbl.create 97 in
-  let rec loop file =
-    let file = canonize file in
-    if not (Hashtbl.mem seen file) then begin
-      Hashtbl.add seen file ();
-      let cin = open_in (file ^ ".v") in
-      let lb = Lexing.from_channel cin in
-      try
-        while true do
-          match coq_action lb with
-            | Require (from, sl) ->
-                List.iter
-                  (fun s ->
-                    match search_v_known ?from s with
-                    | None -> ()
-                    | Some f -> loop f)
-                sl
-            | _ -> ()
-        done
-      with Fin_fichier ->
-        close_in cin;
-        printf "%s%s " file !suffixe
-    end
-  in
-  List.iter (fun (name,_) -> loop name) !vAccu
-
 let usage () =
   eprintf " usage: coqdep [options] <filename>+\n";
   eprintf " options:\n";
@@ -159,8 +117,6 @@ let coqdep () =
   List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
   List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu;
   List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu;
-  warning_mult ".mli" iter_mli_known;
-  warning_mult ".ml" iter_ml_known;
   if !option_sort then begin sort (); exit 0 end;
   if !option_c then mL_dependencies ();
   coq_dependencies ();
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index bd72a52adf..5ece595f13 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -125,8 +125,8 @@ let mkknown () =
     with Not_found -> None
   in add, iter, search
 
-let add_ml_known, iter_ml_known, search_ml_known = mkknown ()
-let add_mli_known, iter_mli_known, search_mli_known = mkknown ()
+let add_ml_known, _, search_ml_known = mkknown ()
+let add_mli_known, _, search_mli_known = mkknown ()
 let add_mllib_known, _, search_mllib_known = mkknown ()
 let add_mlpack_known, _, search_mlpack_known = mkknown ()
 
@@ -616,3 +616,30 @@ let rec treat_file old_dirname old_name =
            | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
            | _ -> ())
     | _ -> ()
+
+let sort () =
+  let seen = Hashtbl.create 97 in
+  let rec loop file =
+    let file = canonize file in
+    if not (Hashtbl.mem seen file) then begin
+      Hashtbl.add seen file ();
+      let cin = open_in (file ^ ".v") in
+      let lb = Lexing.from_channel cin in
+      try
+        while true do
+          match coq_action lb with
+            | Require (from, sl) ->
+                List.iter
+                  (fun s ->
+                    match search_v_known ?from s with
+                    | None -> ()
+                    | Some f -> loop f)
+                sl
+            | _ -> ()
+        done
+      with Fin_fichier ->
+        close_in cin;
+        printf "%s%s " file !suffixe
+    end
+  in
+  List.iter (fun (name,_) -> loop name) !vAccu
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 96266b8e36..1820db4a1e 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -20,44 +20,34 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a
     twice.*)
 val find_dir_logpath: string -> string list
 
+(** Options *)
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
-
 val write_vos : bool ref
-(** output vos and vok dependencies *)
+val suffixe : string ref
 
 type dynlink = Opt | Byte | Both | No | Variable
-
 val option_dynlink : dynlink ref
+
 val norec_dirs : StrSet.t ref
-val suffixe : string ref
+
 type dir = string option
-val get_extension : string -> string list -> string * string
-val basename_noext : string -> string
+val treat_file : dir -> string -> unit
+
+(** ML-related manipulation *)
 val mlAccu : (string * string * dir) list ref
 val mliAccu : (string * dir) list ref
 val mllibAccu : (string * dir) list ref
-val vAccu : (string * string) list ref
-val addQueue : 'a list ref -> 'a -> unit
 val add_ml_known : string -> dir -> string -> unit
-val iter_ml_known : (string -> dir -> unit) -> unit
-val search_ml_known : string -> dir option
 val add_mli_known : string -> dir -> string -> unit
-val iter_mli_known : (string -> dir -> unit) -> unit
-val search_mli_known : string -> dir option
 val add_mllib_known : string -> dir -> string -> unit
-val search_mllib_known : string -> dir option
-val search_v_known : ?from:string list -> string list -> string option
-val file_name : string -> string option -> string
-val escape : string -> string
-val canonize : string -> string
 val mL_dependencies : unit -> unit
+
 val coq_dependencies : unit -> unit
-val suffixes : 'a list -> 'a list list
 val add_known : bool -> string -> string list -> string -> unit
 val add_coqlib_known : bool -> string -> string list -> string -> unit
-val add_caml_known : string -> string list -> string -> unit
+
 val add_caml_dir : string -> unit
 
 (** Simply add this directory and imports it, no subdirs. This is used
@@ -73,5 +63,4 @@ val add_rec_dir_no_import :
 val add_rec_dir_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 
-val treat_file : dir -> string -> unit
-val error_cannot_parse : string -> int * int -> 'a
+val sort : unit -> unit