diff options
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotationsLexer.tokens')
| -rw-r--r-- | doc/tools/coqrst/notations/TacticNotationsLexer.tokens | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens index 4d41a3883..76ed2b065 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens @@ -1,8 +1,9 @@ LGROUP=1 LBRACE=2 RBRACE=3 -ATOM=4 -ID=5 -WHITESPACE=6 +METACHAR=4 +ATOM=5 +ID=6 +WHITESPACE=7 '{'=2 '}'=3 |