3 files changed, 28 insertions, 3 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index b7f6ec250d..2798e4af67 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -22,6 +22,8 @@ let rec parse = function
   | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
+  | "-mldep" :: ocamldep :: ll ->
+      option_mldep := Some ocamldep; option_c := true; parse ll
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 8756d864d1..95c794ca7c 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -26,6 +26,7 @@ let option_c = ref false
 let option_noglob = ref false
 let option_slash = ref false
 let option_natdynlk = ref true
+let option_mldep = ref None
 
 let norecdir_list = ref ([]:string list)
 
@@ -176,7 +177,22 @@ let depend_ML str =
 	(" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
-let traite_fichier_ML md ext =
+let soustraite_fichier_ML dep md ext =
+  try
+    let chan = open_process_in (dep^" -modules "^md^ext) in
+    let list = ocamldep_parse (Lexing.from_channel chan) in
+    let a_faire = ref "" in
+    let a_faire_opt = ref "" in
+    List.iter
+      (fun str ->
+	 let byte,opt = depend_ML str in
+	 a_faire := !a_faire ^ byte;
+	 a_faire_opt := !a_faire_opt ^ opt)
+      (List.rev list);
+    (!a_faire, !a_faire_opt)
+  with Sys_error _ -> ("","")
+
+let autotraite_fichier_ML md ext =
   try
     let chan = open_in (md ^ ext) in
     let buf = Lexing.from_channel chan in
@@ -201,6 +217,11 @@ let traite_fichier_ML md ext =
     (!a_faire, !a_faire_opt)
   with Sys_error _ -> ("","")
 
+let traite_fichier_ML md ext =
+  match !option_mldep with
+    | Some dep -> soustraite_fichier_ML dep md ext
+    | None -> autotraite_fichier_ML md ext
+
 let traite_fichier_mllib md ext =
   try
     let chan = open_in (md ^ ext) in
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 89eeed54ab..74c556a7d2 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -225,8 +225,10 @@ and qual_id = parse
 and mllib_list = parse
   | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }
+  | "*predef*" { mllib_list lexbuf }
   | space+ { mllib_list lexbuf }
   | eof { [] }
 
-
-
+and ocamldep_parse = parse
+  | [^ ':' ]* ':' { mllib_list lexbuf }
+  | _ { [] }