Imported Upstream version 8.5upstream/8.5

1 files changed, 21 insertions, 3 deletions

diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index d610a055..97bdfaef 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,6 +8,14 @@
 
 module StrSet : Set.S with type elt = string
 
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+    if it has been given one. Raise [Not_found] otherwise. In
+    particular we can check if "." has been attributed a logical path
+    after processing all options and silently give the default one if
+    it hasn't. We may also use this to warn if ap hysical path is met
+    twice.*)
+val find_dir_logpath: string -> string list
+
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
@@ -47,9 +55,19 @@ val add_directory :
   bool ->
   (string -> string list -> string -> unit) -> string -> string list -> unit
 val add_caml_dir : string -> unit
-val add_dir :
+
+(** Simply add this directory and imports it, no subdirs. This is used
+    by the implicit adding of the current path. *)
+val add_norec_dir_import :
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
+(** -Q semantic: go in subdirs but only full logical paths are known. *)
+val add_rec_dir_no_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-val add_rec_dir :
+
+(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
+val add_rec_dir_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
 val treat_file : dir -> string -> unit
 val error_cannot_parse : string -> int * int -> 'a