Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.

3 files changed, 34 insertions, 26 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 35a605ddd..32de15ee3 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
           :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
           induction principles.
 
-``.. prodn::`` :black_nib: Grammar productions.
+``.. prodn::`` A grammar production.
     This is useful if you intend to document individual grammar productions.
     Otherwise, use Sphinx's `production lists
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
 
+    Unlike ``.. productionlist``\ s, this directive accepts notation syntax.
+
+
+    Usage::
+
+       .. prodn:: token += production
+       .. prodn:: token ::= production
+
+    Example::
+
+        .. prodn:: term += let: @pattern := @term in @term
+        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+
 ``.. tacn::`` :black_nib: A tactic, or a tactic notation.
     Example::
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 47d3a7d7c..6a9b343ba 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The
 axioms. The optional list of modifiers is used to tailor the behavior
 of the tactic. The following list describes their syntax and effects:
 
-.. prodn::
-   ring_mod ::= abstract %| decidable @term %| morphism @term
-                %| setoid @term @term 
-                %| constants [@ltac] 
-                %| preprocess [@ltac]
-                %| postprocess [@ltac]
-                %| power_tac @term [@ltac] 
-                %| sign @term
-                %| div @term
-
+.. productionlist:: coq
+   ring_mod : abstract | decidable `term` | morphism `term`
+            : | setoid `term` `term`
+            : | constants [`ltac`]
+            : | preprocess [`ltac`]
+            : | postprocess [`ltac`]
+            : | power_tac `term` [`ltac`]
+            : | sign `term`
+            : | div `term`
 
 abstract
   declares the ring as abstract. This is the default.
@@ -663,8 +662,8 @@ messages. :n:`@term` is a proof that the field signature satisfies the
 (semi-)field axioms. The optional list of modifiers is used to tailor
 the behavior of the tactic.
 
-.. prodn::
-   field_mod := @ring_mod %| completeness @term
+.. productionlist:: coq
+   field_mod : `ring_mod` | completeness `term`
 
 Since field tactics are built upon ``ring``
 tactics, all modifiers of the ``Add Ring`` apply. There is only one
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 1c554acdb..ab52c2ce7 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1484,7 +1484,7 @@ The abstract tactic
 ```````````````````
 
 .. tacn:: abstract: {+ d_item}
-   :name abstract (ssreflect)
+   :name: abstract (ssreflect)
 
 This tactic assigns an abstract constant previously introduced with the ``[:
 name ]`` intro pattern (see section :ref:`introduction_ssr`).
@@ -2402,7 +2402,7 @@ tactic:
 The behavior of the defective have tactic makes it possible to
 generalize it in the following general construction:
 
-.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @binder } } {? : @term } {? := @term | by @tactic }
+.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic }
 
 Open syntax is supported for both :token:`term`. For the description
 of :token:`i_item` and :token:`s_item` see section
@@ -5242,7 +5242,7 @@ Notation scope
 
 Module name
 
-.. prodn:: name ::= @qualid
+.. prodn:: modname ::= @qualid
 
 Natural number
 
@@ -5252,14 +5252,10 @@ where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral
 (should not be the name of a tactic which can be followed by a
 bracket ``[``, like ``do``, ``have``,…)
 
-Pattern
-
-.. prodn:: pattern ::= @term
-
 Items and switches
 ~~~~~~~~~~~~~~~~~~
 
-.. prodn:: binder ::= @ident %| ( @ident {? : @term } )
+.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } )
 
 binder see :ref:`abbreviations_ssr`.
 
@@ -5354,8 +5350,8 @@ case analysis see :ref:`the_defective_tactics_ssr`
 
 rewrite  see :ref:`rewriting_ssr`
 
-.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } {? : @term } := @term
-.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } : @term {? by @tactic }
+.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term
+.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic }
 .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term
 .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic }
@@ -5369,9 +5365,9 @@ forward  chaining see :ref:`structure_ssr`
 
 specializing see :ref:`structure_ssr`
 
-.. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+.. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic }
    :name: suff
-.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic }
    :name: suffices
 .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 .. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
@@ -5382,7 +5378,7 @@ backchaining see :ref:`structure_ssr`
 
 local definition :ref:`definitions_ssr`
 
-.. tacv:: pose @ident {+ @binder } := @term
+.. tacv:: pose @ident {+ @ssr_binder } := @term
 
 local function definition