aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools/coqrst/notations/TacticNotations.tokens
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.tokens')
-rw-r--r--doc/tools/coqrst/notations/TacticNotations.tokens3
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