diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /tools/coqdep_lexer.mll | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
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 } | _ |