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

3 files changed, 11 insertions, 9 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index dbe714c388..a8d5ac610f 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -798,7 +798,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in
 
    Notation "[ e ]" := e (e custom expr).
 
-in which case Coq tries to infer it.
+in which case Coq infer it. If the sub-expression is at a border of
+the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is
+determined by the associativity. If the sub-expression is not at the
+border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is
+inferred to be the highest level used for the entry. In particular,
+this level depends on the highest level existing in the entry at the
+time of use of the notation.
 
 In the absence of an explicit entry for parsing or printing a
 sub-expression of a notation in a custom entry, the default is to
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 ->