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 | 17 |
1 files changed, 0 insertions, 17 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 deleted file mode 100644 index eeb4c755f6..0000000000 --- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst +++ /dev/null @@ -1,17 +0,0 @@ -- **Fixed:** Parsing and printing consistently handle inheritance of implicit - arguments in notations. With the exception of notations of - 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 :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:** Notation scopes are now always inherited in - notations binding a partially applied constant, including for - 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>`_). |