summaryrefslogtreecommitdiff
path: root/tools/coqdep_common.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
commit164c6861860e6b52818c031f901ffeff91fca16a (patch)
tree4f91d20c890c25915e7b28226c663b94a8cfb0d3 /tools/coqdep_common.mli
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'tools/coqdep_common.mli')
-rw-r--r--tools/coqdep_common.mli24
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