From 8031bc3963e2c25e04775f5445cc11ad8b5d83e1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 9 Dec 2019 17:10:26 +0100 Subject: Apply and generalize suggestions from Théo. Co-Authored-By: Théo Zimmermann --- .../11120-master+refactoring-application-printing.rst | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'doc') 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 `_, by Hugo Herbelin, fixing `#4690 `_ and `#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 `_). -- cgit v1.2.3