diff options
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.g')
| -rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.g | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 5176c51d2..68658fe49 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -26,7 +26,7 @@ hole: ID; LGROUP: '{' [+*?]; LBRACE: '{'; RBRACE: '}'; -METACHAR: '%' [|()]; +METACHAR: '%' [|(){}]; ATOM: '@' | ~[@{} ]+; ID: '@' [a-zA-Z0-9_]+; WHITESPACE: ' '+; |