diff options
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.g')
| -rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.g | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 905b52525a..f9cf26a21e 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -42,7 +42,8 @@ LALT: '{|'; LGROUP: '{+' | '{*' | '{?'; LBRACE: '{'; RBRACE: '}'; -ESCAPED: '%{' | '%}' | '%|'; +// todo: need a cleaner way to escape the 3-character strings here +ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{'; PIPE: '|'; ATOM: '@' | '_' | ~[@_{}| ]+; ID: '@' ('_'? [a-zA-Z0-9])+; |