diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 2 |
2 files changed, 1 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 13a9ca9fb7..0ec5584faf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -457,11 +457,6 @@ GEXTEND Gram | IDENT "Reset"; IDENT "Section"; id = identarg -> <:ast< (ResetSection $id) >> -(* Extraction *) - | IDENT "Extraction"; id = identarg -> - <:ast< (PrintExtractId $id) >> - | IDENT "Extraction" -> <:ast< (PrintExtract) >> - (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> <:ast< (DebugOn) >> | IDENT "Debug"; IDENT "Off" -> <:ast< (DebugOff) >> diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 570e047116..3f1f952497 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -177,7 +177,7 @@ let get_buff len = String.sub !buff 0 len let rec ident len = parser | [< ' ('a'..'z' | 'A'..'Z' | '\192'..'\214' | '\216'..'\246' - |'\248'..'\255' | '0'..'9' | ''' | '_' as c); s >] -> + |'\248'..'\255' | '0'..'9' | ''' | '_' | '@' as c); s >] -> ident (store len c) s | [< >] -> len |