commit du calcul des dependances un peu plus robuste

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 12 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index c92b30d87c..c66f146f74 100755
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -32,16 +32,6 @@ let suffixe_spec = ref ".vi"
 
 type dir = string option
 
-(* Mapping from logical path to directory name *)
-let rec_path = ref ([] : (string * string) list)
-
-let path_to_file = function
-  | [f] -> f
-  | lpath::relpath as l ->
-      (try String.concat "/" (List.assoc lpath !rec_path :: relpath)
-      with Not_found -> String.concat "/" l)
-  | _ -> assert false
-
 (* Files specified on the command line *)
 let mlAccu  = ref ([] : (string * string * dir) list) 
 and mliAccu = ref ([] : (string * string * dir) list) 
@@ -70,6 +60,12 @@ and coqlibKnown = ref ([] : (string list * string) list)
 let clash_v = ref ([]: (string list * string list) list)
 
 
+let warning_module_notfound f s =
+  eprintf "*** Warning : in file %s, mdule " f;
+  eprintf "%s.v is required and has not been found in loadpath !\n"
+    (String.concat "." s);
+  flush stderr
+
 let warning_notfound f s =
   eprintf "*** Warning : in file %s, the file " f;
   eprintf "%s.v is required and has not been found !\n" s;
@@ -185,7 +181,7 @@ let traite_fichier_Coq verbose f =
                     (if spec then !suffixe_spec else !suffixe)
                 with Not_found -> 
 		  if verbose && not (List.mem_assoc str !coqlibKnown) then
-                    warning_notfound f (path_to_file str)
+                    warning_module_notfound f str
        	      end
 	  | RequireString (spec,s) -> 
 	      let str = Filename.basename s in
@@ -491,7 +487,6 @@ let coqdep () =
         | _ -> ()
   in
   let add_rec_directory dir_name log_name =
-    addQueue rec_path (log_name, dir_name);
     List.iter add_directory (all_subdirs dir_name log_name)
   in
   let rec parse = function