Fixing bug #4265: "coqdep does not handle From ... Require" for good.

3 files changed, 27 insertions, 20 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index ec8e983ec..99b6c7e06 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -36,14 +36,6 @@ let warning_mult suf iter =
   in
   iter check
 
-let add_coqlib_known recur phys_dir log_dir f =
-  match get_extension f [".vo"] with
-    | (basename,".vo") ->
-        let name = log_dir@[basename] in
-	let paths = if recur then suffixes name else [name] in
-        List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
-    | _ -> ()
-
 let sort () =
   let seen = Hashtbl.create 97 in
   let rec loop file =
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0868c9e11..d88455852 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -138,24 +138,31 @@ let get_prefix p l =
   in
   drop_prefix_rec (p, l)
 
-exception Found of string
-
-let search_v_known ?from s = match from with
-| None -> fst (Hashtbl.find vKnown s)
+let search_table (type r) is_root table ?from s = match from with
+| None -> Hashtbl.find table s
 | Some from ->
-  let iter logpath (phys_dir, root) =
-    if root then match get_prefix from logpath with
+  let module M = struct exception Found of r end in
+  let iter logpath binding =
+    if is_root binding then match get_prefix from logpath with
     | None -> ()
     | Some rem ->
       match get_prefix (List.rev s) (List.rev rem) with
       | None -> ()
-      | Some _ -> raise (Found phys_dir)
+      | Some _ -> raise (M.Found binding)
   in
-  try Hashtbl.iter iter vKnown; raise Not_found
-  with Found s -> s
+  try Hashtbl.iter iter table; raise Not_found
+  with M.Found s -> s
 
 let search_v_known ?from s =
-  try Some (search_v_known ?from s) with Not_found -> None
+  let is_root (_, root) = root in
+  try
+    let (phys_dir, _) = search_table is_root vKnown ?from s in
+    Some phys_dir
+  with Not_found -> None
+
+let is_in_coqlib ?from s =
+  let is_root _ = true in
+  try search_table is_root coqlibKnown ?from s; true with Not_found -> false
 
 let clash_v = ref ([]: (string list * string list) list)
 
@@ -353,7 +360,7 @@ let rec traite_fichier_Coq suffixe verbose f =
                     let file_str = safe_assoc from verbose f str in
                     printf " %s%s" (canonize file_str) suffixe
                   with Not_found ->
-		    if verbose && not (Hashtbl.mem coqlibKnown str) then
+		    if verbose && not (is_in_coqlib ?from str) then
                       warning_module_notfound f str
        		end) strl
 	  | Declare sl ->
@@ -466,6 +473,14 @@ let add_caml_known phys_dir _ f =
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
     | _ -> ()
 
+let add_coqlib_known recur phys_dir log_dir f =
+  match get_extension f [".vo"] with
+    | (basename,".vo") ->
+        let name = log_dir@[basename] in
+        let paths = if recur then suffixes name else [name] in
+        List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
+    | _ -> ()
+
 let add_known recur phys_dir log_dir f =
   match get_extension f [".v";".vo"] with
     | (basename,".v") ->
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 23619d1e6..5e5c4740c 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -32,7 +32,6 @@ 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 coqlibKnown : (string list, unit) Hashtbl.t
 val file_name : string -> string option -> string
 val escape : string -> string
 val canonize : string -> string
@@ -40,6 +39,7 @@ 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_directory :
   bool ->