diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-03 17:43:10 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-09 09:07:13 +0200 |
| commit | c928c773b466369d8029ad8e4cd9022fa164f568 (patch) | |
| tree | 6130da5b557fb8b6a69b4e41ea10e7ad92a5e030 /doc/tools/coqrst/notations/TacticNotations.g | |
| parent | ca7a7ffbf5e0576e2a50052e644c1d067843fddf (diff) | |
[Sphinx] Make it possible to espace { by %{ in custom grammars
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: ' '+; |