aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-07-24 15:41:11 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-07-24 15:54:18 +0200
commitd0f9a5523bf16b18bfdf8f427b0e5f005336fa39 (patch)
tree6f58f9d379c67ab71cce020ed15cffa15e40b573 /tools/coqdep_common.mli
parent4456b5edc3e2e62624e5251ff1e01dd81fabb29b (diff)
Fixing bug #4265: "coqdep does not handle From ... Require" for good.
Diffstat (limited to 'tools/coqdep_common.mli')
-rw-r--r--tools/coqdep_common.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 23619d1e6..5e5c4740c 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -32,7 +32,6 @@ val search_mli_known : string -> dir option
val add_mllib_known : string -> dir -> string -> unit
val search_mllib_known : string -> dir option
val search_v_known : ?from:string list -> string list -> string option
-val coqlibKnown : (string list, unit) Hashtbl.t
val file_name : string -> string option -> string
val escape : string -> string
val canonize : string -> string
@@ -40,6 +39,7 @@ val mL_dependencies : unit -> unit
val coq_dependencies : unit -> unit
val suffixes : 'a list -> 'a list list
val add_known : bool -> string -> string list -> string -> unit
+val add_coqlib_known : bool -> string -> string list -> string -> unit
val add_caml_known : string -> string list -> string -> unit
val add_directory :
bool ->