From bc480bb7068b0ffeeb8ad5cb90ee73fabc068d5f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 1 Jul 2018 11:10:36 +0200
Subject: Do not treat curly brackets specially in custom entries.

---
 vernac/metasyntax.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 7c1a880c46..67506a2551 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1229,7 +1229,8 @@ let compute_syntax_data df modifiers =
   let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
   let custom = make_custom_entry mods.custom n in
   let ntn_for_interp = make_notation_key custom symbols in
-  let symbols_for_grammar = remove_curly_brackets symbols in
+  let symbols_for_grammar =
+    if custom = InConstrEntrySomeLevel then remove_curly_brackets symbols else symbols in
   let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
   let ntn_for_grammar = if need_squash then make_notation_key custom symbols_for_grammar else ntn_for_interp in
   if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar;
-- 
cgit v1.2.3