From 039b2423cf7b85f2f5960dde6a1586f0f07cf9d0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 29 Sep 2019 00:06:19 +0200 Subject: Addressing #6082 and #7766 (overriding format of notation). We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format. --- doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a8d5ac610f..04419f08f7 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -163,6 +163,10 @@ Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast, it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: +.. coqtop:: none + + Reset Initial. + .. coqtop:: all Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). -- cgit v1.2.3 From 8364b7fea91a11ad07d94057f3a5a938b9524d81 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Nov 2019 22:09:07 +0100 Subject: Short allusion in refman on the existence of a generic and specific format. --- doc/sphinx/user-extensions/syntax-extensions.rst | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 04419f08f7..7c628e534b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -354,6 +354,11 @@ Reserving notations This command declares an infix parsing rule without giving its interpretation. + When a format is attached to a reserved notation, it is used by + default by all subsequent interpretations of the corresponding + notation. A specific interpretation can provide its own format + overriding the default format though. + Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From a91c22fcfd5df6153cc9f1b1b4e3d9840055bf0d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Nov 2019 22:12:47 +0100 Subject: Adding change log for #10832. --- .../10832-master+fix6082-7766-overriding-notation-format.rst | 1 + 1 file changed, 1 insertion(+) create mode 100644 doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst new file mode 100644 index 0000000000..5393fb3d8c --- /dev/null +++ b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst @@ -0,0 +1 @@ +- Different interpretations in different scopes of the same notation string can now be associated to different printing formats; this fixes bug #6092 and #7766 (`#10832 `_, by Hugo Herbelin). -- cgit v1.2.3