Prise en compte du Require multiple

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

1 files changed, 18 insertions, 13 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2b5d192db6..f8ee39a582 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -162,8 +162,12 @@ let sort () =
       try
 	while true do
 	  match coq_action lb with
-	    | Require (_, s) ->
-		(try loop (List.assoc s !vKnown) with Not_found -> ())
+	    | Require (_, sl) ->
+		List.iter 
+		  (fun s -> 
+		    try loop (List.assoc s !vKnown) 
+		    with Not_found -> ())
+		sl
 	    | RequireString (_, s) -> loop s
 	    | _ -> ()
 	done
@@ -184,17 +188,18 @@ let traite_fichier_Coq verbose f =
       while true do
       	let tok = coq_action buf in
 	match tok with
-	  | Require (spec,str) ->
-	      if not (List.mem str !deja_vu_v) then begin
-	        addQueue deja_vu_v str;
-                try
-                  let file_str = safe_assoc verbose f str in
-                  printf " %s%s" (canonize file_str)
-                    (if spec then !suffixe_spec else !suffixe)
-                with Not_found -> 
-		  if verbose && not (List.mem_assoc str !coqlibKnown) then
-                    warning_module_notfound f str
-       	      end
+	  | Require (spec,strl) ->
+	      List.iter (fun str ->
+		if not (List.mem str !deja_vu_v) then begin
+	          addQueue deja_vu_v str;
+                  try
+                    let file_str = safe_assoc verbose f str in
+                    printf " %s%s" (canonize file_str)
+                      (if spec then !suffixe_spec else !suffixe)
+                  with Not_found -> 
+		    if verbose && not (List.mem_assoc str !coqlibKnown) then
+                      warning_module_notfound f str
+       		end) strl
 	  | RequireString (spec,s) -> 
 	      let str = Filename.basename s in
 	      if not (List.mem [str] !deja_vu_v) then begin