diff options
| author | Pierre-Marie Pédrot | 2016-02-24 10:26:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-24 10:31:17 +0100 |
| commit | d96bf1b1ec79fa93787d23e1c42f803d74b49321 (patch) | |
| tree | 96f23cdf57def01387e8ad7155ba5305bb3ec132 /parsing/lexer.ml4 | |
| parent | ee162ba3b28fccca0a2b3ea4b1e0811006840570 (diff) | |
Removing the METAIDENT token, as it is not used anymore.
METAIDENT were idents of the form $foobar, only used in quotations.
Note that it removes two dollars in the Coq codebase! Guess I'm absolved
for the $(...) syntax.
Diffstat (limited to 'parsing/lexer.ml4')
| -rw-r--r-- | parsing/lexer.ml4 | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 74e05ce84d..232e9aee3f 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -493,7 +493,6 @@ let process_chars bp c cs = err (bp, ep') Undefined_token let token_of_special c s = match c with - | '$' -> METAIDENT s | '.' -> FIELD s | _ -> assert false @@ -532,8 +531,6 @@ let blank_or_eof cs = let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$' as c; t = parse_after_special c bp >] ep -> - comment_stop bp; (t, (ep, bp)) | [< ''.' as c; t = parse_after_special c bp; s >] ep -> comment_stop bp; (* We enforce that "." should either be part of a larger keyword, |