Coqdep: update include strategies

-I is (only) the ml one
-I -as is fixed
-Q is understood
-R is not a recursive ml include anymore

$COQENV, user_contrib, ... are not recursively included

coqlib/theories and coqlib/plugins are still recursively included (for now). (This
may deserves an option)

Closes Bug 2910: If there is a "Require a." in a b.v and a a.vo in path but no a.v,
coqdep does not complains about a missing a.v.

1 files changed, 15 insertions, 10 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index febde9b69..a44f159b4 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -36,11 +36,11 @@ let warning_mult suf iter =
   in
   iter check
 
-let add_coqlib_known phys_dir log_dir f =
+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 = suffixes name in
+	let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
@@ -445,16 +445,19 @@ let rec parse = function
   | "-c" :: ll -> option_c := true; parse ll
   | "-D" :: ll -> option_D := true; parse ll
   | "-w" :: ll -> option_w := true; parse ll
-  | "-boot" :: ll -> Flags.boot := true; parse ll
+  | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
-  | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r (split_period ln); parse ll
+  | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [];
+    add_dir add_known r (split_period ln);
+    parse ll
   | "-I" :: r :: "-as" :: [] -> usage ()
-  | "-I" :: r :: ll -> add_dir add_known r []; parse ll
+  | "-I" :: r :: ll -> add_caml_dir r; parse ll
   | "-I" :: [] -> usage ()
   | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
   | "-R" :: r :: "-as" :: [] -> usage ()
   | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
+  | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll
   | "-R" :: ([] | [_]) -> usage ()
   | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
   | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
@@ -476,19 +479,21 @@ let coqdep () =
   parse (List.tl (Array.to_list Sys.argv));
   if not Coq_config.has_natdynlink then option_natdynlk := false;
   (* NOTE: These directories are searched from last to first *)
-  if !Flags.boot then begin
+  if !option_boot then begin
     add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "plugins" ["Coq"]
+    add_rec_dir add_known "plugins" ["Coq"];
+    add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
+    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
   end else begin
     Envars.set_coqlib ~fail:Errors.error;
     let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
-    if Sys.file_exists user then add_rec_dir add_coqlib_known user [];
-    List.iter (fun s -> add_rec_dir add_coqlib_known s [])
+    if Sys.file_exists user then add_dir add_coqlib_known user [];
+    List.iter (fun s -> add_dir add_coqlib_known s [])
       (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
-    List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath;
+    List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
   List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;