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, 6 insertions, 3 deletions

diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 3e4ffe500..3c1cd4fbe 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -8,6 +8,7 @@
 
 val option_c : bool ref
 val option_noglob : bool ref
+val option_boot : bool ref
 val option_natdynlk : bool ref
 val option_mldep : string option ref
 val norec_dirs : string list ref
@@ -38,13 +39,15 @@ val canonize : string -> string
 val mL_dependencies : unit -> unit
 val coq_dependencies : unit -> unit
 val suffixes : 'a list -> 'a list list
-val add_known : string -> string list -> string -> unit
+val add_known : bool -> string -> string list -> string -> unit
+val add_caml_known : string -> string list -> string -> unit
 val add_directory :
   bool ->
   (string -> string list -> string -> unit) -> string -> string list -> unit
+val add_caml_dir : string -> unit
 val add_dir :
-  (string -> string list -> string -> unit) -> string -> string list -> unit
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 val add_rec_dir :
-  (string -> string list -> string -> unit) -> string -> string list -> unit
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 val treat_file : dir -> string -> unit
 val error_cannot_parse : string -> int * int -> 'a