From 12d2e91a9018d2189b041249c440d483c14b5575 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Dec 2019 18:11:52 +0100 Subject: Adding a changelog item. --- .../11120-master+refactoring-application-printing.rst | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 doc/changelog/03-notations/11120-master+refactoring-application-printing.rst (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 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 `_, 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 + not the case beforehand + (part of `#11120 `_). -- cgit v1.2.3 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 From 2d51333d75bdcce1c1f53830e7303febd7ec2bf4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 12 Dec 2019 21:06:12 +0100 Subject: Update doc/changelog/03-notations/11120-master+refactoring-application-printing.rst Thanks Co-Authored-By: Jim Fehrle --- .../03-notations/11120-master+refactoring-application-printing.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (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 7bcd13ae4d..7a1d8b508e 100644 --- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst +++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst @@ -1,5 +1,5 @@ - **Fixed:** Inheritance of implicit arguments across notations made - uniform in parsing and printing. To the exception of notations of + uniform in parsing and printing. 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 })`, -- cgit v1.2.3 From 4ef01a6b646b10ed03d40ea8b92d47f05870fcfd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Dec 2019 13:04:55 +0100 Subject: Addressing a changelog comment from Théo Zimmermann. --- .../03-notations/11120-master+refactoring-application-printing.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 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 7a1d8b508e..d95f554766 100644 --- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst +++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst @@ -1,5 +1,5 @@ -- **Fixed:** Inheritance of implicit arguments across notations made - uniform in parsing and printing. With the exception of notations of +- **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 })`, -- cgit v1.2.3 From 9e6637326483d1356376bf8bb2fcf2183d3f345b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 23 Feb 2020 09:13:52 +0100 Subject: Documenting inheritance of implicit arguments and scopes in notations. --- doc/sphinx/user-extensions/syntax-extensions.rst | 27 ++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 7c628e534b..8bfcab0f4e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -417,6 +417,27 @@ identifiers or tokens starting with a single quote are dropped. Locate "exists". Locate "exists _ .. _ , _". +Inheritance of the properties of arguments of constants bound to a notation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +If the right-hand side of a notation is a partially applied constant, +the notation inherits the implicit arguments (see +:ref:`ImplicitArguments`) and interpretation scopes (see +:ref:`Scopes`) of the constant. For instance: + +.. coqtop:: in reset + + Record R := {dom : Type; op : forall {A}, A -> dom}. + Notation "# x" := (@op x) (at level 8). + +.. coqtop:: all + + Check fun x:R => # x 3. + +As an exception, if the right-hand side is just of the form +:n:`@@qualid`, this conventionally stops the inheritance of implicit +arguments (but not of interpretation scopes). + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -1415,6 +1436,12 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + Like for notations, if the right-hand side of an abbreviation is a + partially applied constant, the abbreviation inherits the implicit + arguments and interpretation scopes of the constant. As an + exception, if the right-hand side is just of the form :n:`@@qualid`, + this conventionally stops the inheritance of implicit arguments. + .. _numeral-notations: Numeral notations -- cgit v1.2.3