Adding a changelog item.

1 files changed, 16 insertions, 0 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
new file mode 100644
index 0000000000..b8bef23f67
--- /dev/null
+++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
@@ -0,0 +1,16 @@
+- **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
+  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
+  (`#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
+  not the case beforehand
+  (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).