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

1 files changed, 7 insertions, 1 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