Convert Gallina Vernac to use prodn

2 files changed, 14 insertions, 9 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 5b0b3c51b0..34197c4fcf 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -337,31 +337,31 @@ Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
 
 .. cmd:: Derive Inversion @ident with @ident Sort @sort
-         Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort
+         Derive Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    This command generates an inversion principle for the
    :tacn:`inversion ... using ...` tactic.  The first :token:`ident` is the name
    of the generated principle.  The second :token:`ident` should be an inductive
    predicate, and :token:`binders` the variables occurring in the term
    :token:`term`. This command generates the inversion lemma for the sort
-   :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`.
+   :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`.
    When applied, it is equivalent to having inverted the instance with the
    tactic :g:`inversion`.
 
 .. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort
-          Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
+          Derive Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with the
    tactic inversion replaced by the tactic `inversion_clear`.
 
 .. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort
-          Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort
+          Derive Dependent Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with
    the tactic `dependent inversion`.
 
 .. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort
-          Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
+          Derive Dependent Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance
    with the tactic `dependent inversion_clear`.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 8bfcab0f4e..e1545bdc2b 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -310,10 +310,10 @@ at the time of use of the notation.
 The Infix command
 ~~~~~~~~~~~~~~~~~~
 
-The :cmd:`Infix` command is a shortening for declaring notations of infix
+The :cmd:`Infix` command is a shortcut for declaring notations for infix
 symbols.
 
-.. cmd:: Infix "@symbol" := @term {? (@modifiers) }.
+.. cmd:: Infix @string := @term {? (@modifiers) }
 
    This command is equivalent to
 
@@ -366,7 +366,7 @@ Thanks to reserved notations, the inductive, co-inductive, record, recursive and
 corecursive definitions can benefit from customized notations. To do this, insert
 a ``where`` notation clause after the definition of the (co)inductive type or
 (co)recursive term (or after the definition of each of them in case of mutual
-definitions). The exact syntax is given by :token:`decl_notation` for inductive,
+definitions). The exact syntax is given by :n:`@decl_notation` for inductive,
 co-inductive, recursive and corecursive definitions and in :ref:`record-types`
 for records. Here are examples:
 
@@ -909,7 +909,6 @@ notations are given below. The optional :production:`scope` is described in
                  : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : [Local] Declare Custom Entry `ident`.
-   decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
    modifiers     : `modifier`, … , `modifier`
    modifier      : at level `num`
                  : in custom `ident`
@@ -939,6 +938,12 @@ notations are given below. The optional :production:`scope` is described in
                  : as pattern
                  : as strict pattern
 
+.. insertprodn decl_notations decl_notation
+
+.. prodn::
+   decl_notations ::= where @decl_notation {* and @decl_notation }
+   decl_notation ::= @string := @term1_extended {? : @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.