diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
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 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 ~~~~~~~~~~~~~~~~~~ |