Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

2 files changed, 15 insertions, 1 deletions

diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst
new file mode 100644
index 0000000000..b105928b22
--- /dev/null
+++ b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst
@@ -0,0 +1,8 @@
+- **Fixed:**
+  Bugs in dealing with precedences of notations in custom entries
+  (`#11530 <https://github.com/coq/coq/pull/11530>`_,
+  by Hugo Herbelin, fixing in particular
+  `#9517 <https://github.com/coq/coq/pull/9517>`_,
+  `#9519 <https://github.com/coq/coq/pull/9519>`_,
+  `#9521 <https://github.com/coq/coq/pull/9521>`_,
+  `#11331 <https://github.com/coq/coq/pull/11331>`_).
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