Merge PR #11602: Adding support for an "only parsing" modifier in "where"-based notation

Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot

3 files changed, 16 insertions, 8 deletions

diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
new file mode 100644
index 0000000000..1d30d16664
--- /dev/null
+++ b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Notations declared with the ``where`` clause in the declaration of
+  inductive types, coinductive types, record fields, fixpoints and
+  cofixpoints now support the ``only parsing`` modifier
+  (`#11602 <https://github.com/coq/coq/pull/11602>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 6c1d83b3b8..b9e181dd94 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -24,7 +24,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
      record         : `record_keyword` `record_body` with … with `record_body`
      record_keyword : Record | Inductive | CoInductive
      record_body    : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }.
-     field          : `ident` [ `binders` ] : `type` [ where `notation` ]
+     field          : `ident` [ `binders` ] : `type` [ `decl_notations` ]
                     : `ident` [ `binders` ] [: `type` ] := `term`
 
 .. cmd:: {| Record | Structure } @inductive_definition {* with @inductive_definition }
@@ -35,8 +35,10 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
    the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is
    omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of
    fields. For a given field :token:`ident`, its type is :n:`forall {* @binder }, @type`.
-   Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the
-   order of the fields is important. Finally, :token:`binders` are parameters of the record.
+   Notice that the type of a particular identifier may depend on a previously-given identifier. Thus the
+   order of the fields is important. The record can depend as a whole on parameters :token:`binders`
+   and each field can also depend on its own :token:`binders`. Finally, notations can be attached to
+   fields using the :n:`decl_notations` annotation.
 
    :cmd:`Record` and :cmd:`Structure` are synonyms.
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 9b4d7cf5fa..fd95a5cef4 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -909,10 +909,10 @@ notations are given below. The optional :production:`scope` is described in
    notation      : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`].
                  : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`].
                  : [Local] Reserved Notation `string` [(`modifiers`)] .
-                 : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
-                 : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
-                 : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
-                 : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
+                 : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`].
+                 : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`].
+                 : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`].
+                 : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`].
                  : [Local] Declare Custom Entry `ident`.
    modifiers     : `modifier`, … , `modifier`
    modifier      : at level `num`
@@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in
 
 .. prodn::
    decl_notations ::= where @decl_notation {* and @decl_notation }
-   decl_notation ::= @string := @term1_extended {? : @ident }
+   decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident }
 
 .. note:: No typing of the denoted expression is performed at definition
           time. Type checking is done only at the time of use of the notation.