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_lexer.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_lexer.mli')
| -rw-r--r-- | tools/coqdep_lexer.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index c7b9c9a0a..84c9ba798 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -11,7 +11,7 @@ type mL_token = Use_module of string type qualid = string list type coq_token = - Require of qualid list + Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string |