Do not treat curly brackets specially in custom entries.

1 files changed, 2 insertions, 1 deletions

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;