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 f29c69eeaf..70107eba46 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -43,7 +43,8 @@ LGROUP: '{+' | '{*' | '{?'; LBRACE: '{'; RBRACE: '}'; // todo: need a cleaner way to escape the 3-character strings here -ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{'; +ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{' | + '%|-' | '%|->' | '%||' | '%|||' | '%||||'; // for SSR PIPE: '|'; ATOM: '@' | '_' | ~[@_{}| ]+; ID: '@' ('_'? [a-zA-Z0-9])+; |