Merge PR #12984: [printing] Order notations by matching precision first, and then by last imported

Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares

3 files changed, 38 insertions, 1 deletions

diff --git a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst
new file mode 100644
index 0000000000..d472e6fdf0
--- /dev/null
+++ b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst
@@ -0,0 +1,12 @@
+- **Changed:**
+  Redeclaring a notation reactivates also its printing rule; in
+  particular a second :cmd:`Import` of the same module reactivates the
+  printing rules declared in this module. In theory, this leads to
+  changes of behavior for printing. However, this is mitigated in
+  general by the adoption in `#12986
+  <https://github.com/coq/coq/pull/12986>`_ of a priority given to
+  notations which match a larger part of the term to print
+  (`#12984 <https://github.com/coq/coq/pull/12984>`_,
+  fixes `#7443 <https://github.com/coq/coq/issues/7443>`_
+  and `#10824 <https://github.com/coq/coq/issues/10824>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst
new file mode 100644
index 0000000000..8b233972bf
--- /dev/null
+++ b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Use of notations for printing now gives preference
+  to notations which match a larger part of the term to abbreviate
+  (`#12986 <https://github.com/coq/coq/pull/12986>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 56b14d0935..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
 ~~~~~~~~~~~~~~~~~~