From 5e87ba237e2219527095de0aba8744e5c791ac85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Nov 2020 15:32:27 +0100
Subject: Documenting priority given to most recently declared/imported
 notations.

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 99b9754e5e..2e44955b03 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -323,7 +323,6 @@ 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
@@ -337,6 +336,13 @@ at the time of use of the notation.
 
      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
 ~~~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3