1 files changed, 14 insertions, 10 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens
index 88b38f97a6..2670e20aa6 100644
--- a/doc/tools/coqrst/notations/TacticNotations.tokens
+++ b/doc/tools/coqrst/notations/TacticNotations.tokens
@@ -1,10 +1,14 @@
-LGROUP=1
-LBRACE=2
-RBRACE=3
-METACHAR=4
-ATOM=5
-ID=6
-SUB=7
-WHITESPACE=8
-'{'=2
-'}'=3
+LALT=1
+LGROUP=2
+LBRACE=3
+RBRACE=4
+ESCAPED=5
+PIPE=6
+ATOM=7
+ID=8
+SUB=9
+WHITESPACE=10
+'{|'=1
+'{'=3
+'}'=4
+'|'=6