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.mll | |
| 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.mll')
| -rw-r--r-- | tools/coqdep_lexer.mll | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 5692e5b45..291bc55fb 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -16,7 +16,7 @@ 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 @@ -270,12 +270,9 @@ and require_file = parse module_names := [coq_qual_id_tail lexbuf]; let qid = coq_qual_id_list lexbuf in parse_dot lexbuf; - match !from_pre_ident with - None -> - Require qid - | Some from -> - (from_pre_ident := None ; - Require (List.map (fun x -> from @ x) qid)) } + let from = !from_pre_ident in + from_pre_ident := None; + Require (from, qid) } | eof { syntax_error lexbuf } | _ |