1 files changed, 44 insertions, 5 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index f36767b207..16c8586a9f 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -214,7 +214,7 @@ have to be observed for notations starting with a symbol, e.g., rules
 starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list
 of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`.
 
-Displaying symbolic notations
+Use of notations for printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The command :cmd:`Notation` has an effect both on the Coq parser and on the
@@ -323,6 +323,26 @@ at the time of use of the notation.
    scope. Obviously, expressions printed by means of such extra
    printing rules will not be reparsed to the same form.
 
+.. note::
+
+   When several notations can be used to print a given term, the
+   notations which capture the largest subterm of the term are used
+   preferentially. Here is an example:
+
+   .. coqtop:: in
+
+     Notation "x < y" := (lt x y) (at level 70).
+     Notation "x < y < z" := (lt x y /\ lt y z) (at level 70, y at next level).
+
+     Check (0 < 1 /\ 1 < 2).
+
+   When several notations match the same subterm, or incomparable
+   subterms of the term to print, the notation declared most recently
+   is selected. Moreover, reimporting a library or module declares the
+   notations of this library or module again. If the notation is in a
+   scope (see :ref:`Scopes`), either the scope has to be opened or a
+   delimiter has to exist in the scope for the notation to be usable.
+
 The Infix command
 ~~~~~~~~~~~~~~~~~~
 
@@ -787,20 +807,39 @@ nested iterating pattern, the second placeholder is finally filled with the
 terminating expression.
 
 In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E\, [~]_I`
-and the terminating expression is ``nil``. Here are other examples:
+and the terminating expression is ``nil``.
+
+Here is another example with the pattern associating on the left:
 
 .. coqtop:: in
 
    Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
 
+Here is an example with more involved recursive patterns:
+
+.. coqtop:: in
+
    Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
      (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
            (pair .. (pair (pair a u) (pair b u)) .. (pair c u)))
      (t at level 39).
 
-Notations with recursive patterns can be reserved like standard
-notations, they can also be declared within
-:ref:`notation scopes <Scopes>`.
+To give a flavor of the extent and limits of the mechanism, here is an
+example showing a notation for a chain of equalities. It relies on an
+artificial expansion of the intended denotation so as to expose a
+``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the
+beta-redexes are contracted, the notations stops to be used for
+printing.
+
+.. coqtop:: in
+
+   Notation "x  ⪯ y  ⪯ ..  ⪯ z  ⪯ t" :=
+     ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x)
+     (at level 70, y at next level, z at next level, t at next level).
+
+Note finally that notations with recursive patterns can be reserved like
+standard notations, they can also be declared within :ref:`notation
+scopes <Scopes>`.
 
 .. _RecursiveNotationsWithBinders: