diff options
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotations.g')
| -rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.g | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 68658fe49..a889ebda7 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -20,13 +20,14 @@ repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; whitespace: WHITESPACE; meta: METACHAR; -atomic: ATOM; -hole: ID; +atomic: ATOM (SUB)?; +hole: ID (SUB)?; LGROUP: '{' [+*?]; LBRACE: '{'; RBRACE: '}'; METACHAR: '%' [|(){}]; -ATOM: '@' | ~[@{} ]+; -ID: '@' [a-zA-Z0-9_]+; +ATOM: '@' | '_' | ~[@_{} ]+; +ID: '@' ('_'? [a-zA-Z0-9])+; +SUB: '_' '_' [a-zA-Z0-9]+; WHITESPACE: ' '+; |