diff options
Diffstat (limited to 'doc/changelog/03-notations/11120-master+refactoring-application-printing.rst')
| -rw-r--r-- | doc/changelog/03-notations/11120-master+refactoring-application-printing.rst | 11 |
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>`_). |