diff options
| -rw-r--r-- | vernac/metasyntax.ml | 3 |
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; |