From c928c773b466369d8029ad8e4cd9022fa164f568 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Tue, 3 Apr 2018 17:43:10 +0200
Subject: [Sphinx] Make it possible to espace { by %{ in custom grammars

---
 doc/tools/coqrst/notations/TacticNotations.g | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools/coqrst/notations/TacticNotations.g')

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: ' '+;
-- 
cgit v1.2.3