diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 3 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 9 |
2 files changed, 4 insertions, 8 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index bf49fb4df5..9f41287bce 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -213,7 +213,8 @@ let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in mat (* If a default level in a different grammar, the entry name is ok *) | (DefaultLevel,InternalProd) -> if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel - | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> DefaultLevel + | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> + if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel (* Associativity is None means force the level *) | (NumLevel n,BorderProd (_,None)) -> NumLevel n | (DefaultLevel,BorderProd (_,None)) -> assert false diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 1e46d35ed7..7794b0a37a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -978,17 +978,12 @@ let is_only_printing mods = let set_entry_type from n etyps (x,typ) = let make_lev n s = match typ with | BorderProd _ -> NumLevel n - | InternalProd -> - if s = InConstrEntry then NumLevel 200 else - user_err (strbrk "level of inner subentry " ++ quote (pr_notation_entry s) ++ - str " cannot be inferred. It must be given explicitly.") in + | InternalProd -> DefaultLevel in let typ = try match List.assoc x etyps, typ with | ETConstr (s,bko,DefaultLevel), _ -> if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ)) - else if s = InConstrEntry then ETConstr (s,bko,(make_lev 200 s,typ)) else - user_err (strbrk "level of subentry " ++ quote (pr_notation_entry s) ++ - str " cannot be inferred. It must be given explicitly.") + else ETConstr (s,bko,(DefaultLevel,typ)) | ETConstr (s,bko,n), BorderProd (left,_) -> ETConstr (s,bko,(n,BorderProd (left,None))) | ETConstr (s,bko,n), InternalProd -> |