Ajout d'un warning losrqu'un nom de bibliothèque est ambigü

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

1 files changed, 22 insertions, 6 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 20c8a84b4d..b258efd6b9 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -98,15 +98,31 @@ let all_subdirs ~unix_path:root =
   List.rev !l
 
 let where_in_path path filename =
-  let rec search = function
+  let rec search acc = function
     | lpe :: rem ->
 	let f = Filename.concat lpe filename in
-	if Sys.file_exists f then (lpe,f) else search rem
-    | [] ->
-	raise Not_found
+	  if Sys.file_exists f 
+	  then (search ((lpe,f)::acc) rem) 
+	  else search acc rem
+    | [] -> acc in
+  let rec check_and_warn cont acc l = 
+    match l with
+      | [] -> if cont then assert false else raise Not_found
+      | [ (lpe, f) ] -> 
+	  if cont then begin
+	      warning (acc ^ (string_of_physical_path lpe) ^ " ]");
+	      warning ("Loading " ^ f)
+	    end;
+	  (lpe, f)
+      | (lpe, f) :: l' -> 
+	  if cont then
+	    check_and_warn true (acc ^ "; ") l'
+	  else
+	    check_and_warn true 
+	      (filename ^ " has been found in [ " ^ (string_of_physical_path lpe) ^ "; ") l' 
   in
-  search path
-
+    check_and_warn false "" (search [] path)
+  
 let find_file_in_path paths filename =
   if not (Filename.is_implicit filename) then
     let root = Filename.dirname filename in