diff options
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.g')
| -rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.g | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 72ae8eb6b..5176c51d2 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -15,16 +15,18 @@ grammar TacticNotations; top: blocks EOF; blocks: block ((whitespace)? block)*; -block: atomic | hole | repeat | curlies; +block: atomic | meta | hole | repeat | curlies; repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; whitespace: WHITESPACE; +meta: METACHAR; atomic: ATOM; hole: ID; LGROUP: '{' [+*?]; LBRACE: '{'; RBRACE: '}'; -ATOM: ~[@{} ]+; +METACHAR: '%' [|()]; +ATOM: '@' | ~[@{} ]+; ID: '@' [a-zA-Z0-9_]+; WHITESPACE: ' '+; |