diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-30 16:39:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-03 04:16:31 +0200 |
| commit | 31c7542731a62f56bd60f443a84d68813f8780a8 (patch) | |
| tree | 869635fac06174b40babe4acc047ec621db5b79a /tools/coqdep_common.mli | |
| parent | 6482ca75a39709e65de676d533b3d115ad2b1153 (diff) | |
Fixing bug #4265: coqdep does not handle From ... Require.
The search algorithm is not satisfactory though, as it crawls through
all known files to find the proper one. We should rather use some trie-based
data structure, but I'll leave this for a future commit.
Diffstat (limited to 'tools/coqdep_common.mli')
| -rw-r--r-- | tools/coqdep_common.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 71b96ca0e..23619d1e6 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -31,7 +31,7 @@ val iter_mli_known : (string -> dir -> unit) -> unit val search_mli_known : string -> dir option val add_mllib_known : string -> dir -> string -> unit val search_mllib_known : string -> dir option -val vKnown : (string list, string) Hashtbl.t +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 |