diff options
Diffstat (limited to 'tools/coqdep_lexer.mll')
| -rw-r--r-- | tools/coqdep_lexer.mll | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 8ecc419c..291bc55f 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -16,8 +16,7 @@ type qualid = string list type coq_token = - | Require of qualid list - | RequireString of string + | Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string @@ -271,16 +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 s = Lexing.lexeme lexbuf in - parse_dot lexbuf; - RequireString (unquote_vfile_string s) } + let from = !from_pre_ident in + from_pre_ident := None; + Require (from, qid) } | eof { syntax_error lexbuf } | _ |