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/sphinx')

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/sphinx')

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