Apply and generalize suggestions from Théo.

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>

1 files changed, 6 insertions, 5 deletions

diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
index b8bef23f67..7bcd13ae4d 100644
--- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
+++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
@@ -1,16 +1,17 @@
 - **Fixed:** Inheritance of implicit arguments across notations made
   uniform in parsing and printing. To the exception of notations of
-  the form ``Notation "..." := @foo`` and ``Notation id := @foo`` which
+  the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
   inhibit implicit arguments, all notations binding a partially
-  applied constant, as e.g. in ``Notation "..." := (foo args)``,
-  or ``Notation "..." := (@foo args)``, or ``Notation id := (foo args)``, or
-  ``Notation id := (@foo args)``, inherits the remaining implicit arguments
+  applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
+  or :n:`Notation @string := (@@qualid {+ @arg })`, or
+  :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident
+  := (@@qualid {+ @arg })`, inherit the remaining implicit arguments
   (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo
   Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and
   `#11091 <https://github.com/coq/coq/pull/11091>`_).
 
 - **Changed:** Interpretation scopes are now always inherited in
   notations binding a partially applied constant, including for
-  notations binding an expression of the form ``@foo``. The latter was
+  notations binding an expression of the form :n:`@@qualid`. The latter was
   not the case beforehand
   (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).