Custom entries: accept that no level is mentioned for a subentry.

If it is for an internal non-terminal then:
- if for a subentry different from constr, it refers to the head of
  the subentry
- if in constr, it is 200 by convention

If it is on the border of a rule, then:
- if it is in a subentry different from the entry it lives, it refers
  to the head of the subentry (or 200 by convention if in constr)
- if it is in the same entry, the rule for associativity tells if a
  SELF, a NEXT, or (if on the right) a LEVEL

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 ->