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