Convert Gallina Vernac to use prodn

4 files changed, 20 insertions, 21 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b722b1af74..56e33b9ea5 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -907,9 +907,9 @@ Ltac2 from Ltac1
 Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
 instead.
 
-.. productionlist:: coq
-  ltac_expr : ltac2 : ( `ltac2_term` )
-            : ltac2 : ( `ident` ... `ident` |- `ltac2_term` )
+.. prodn::
+   ltac_expr += ltac2 : ( `ltac2_term` )
+   | ltac2 : ( `ident` ... `ident` |- `ltac2_term` )
 
 The typing rules are dual, that is, the optional identifiers are bound
 with type `Ltac2.Ltac1.t` in the Ltac2 expression, which is expected to have
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index b1734b3f19..03eebc32f9 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -80,20 +80,19 @@ list of assertion commands is given in :ref:`Assertions`. The command
       a while when the proof is large. In some exceptional cases one may
       even incur a memory overflow.
 
-   .. cmdv:: Defined
-      :name: Defined
+.. cmd:: Defined
 
-      Same as :cmd:`Qed` but the proof is then declared transparent, which means
-      that its content can be explicitly used for type checking and that it can be
-      unfolded in conversion tactics (see :ref:`performingcomputations`,
-      :cmd:`Opaque`, :cmd:`Transparent`).
+   Same as :cmd:`Qed`, except the proof is made *transparent*, which means
+   that its content can be explicitly used for type checking and that it can be
+   unfolded in conversion tactics (see :ref:`performingcomputations`,
+   :cmd:`Opaque`, :cmd:`Transparent`).
 
-   .. cmdv:: Save @ident
-      :name: Save
+.. cmd:: Save @ident
+   :name: Save
 
-      Forces the name of the original goal to be :token:`ident`. This
-      command (and the following ones) can only be used if the original goal
-      has been opened using the :cmd:`Goal` command.
+   Forces the name of the original goal to be :token:`ident`. This
+   command can only be used if the original goal
+   was opened using the :cmd:`Goal` command.
 
 .. cmd:: Admitted
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 46215f16a6..90a991794f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1702,7 +1702,7 @@ Intro patterns
   when it is the
   very *first* :token:`i_pattern` after tactic ``=>`` tactical *and* tactic
   is not a move, is a *branching*:token:`i_pattern`. It executes the sequence
-  :token:`i_item`:math:`_i` on the i-th   subgoal produced by tactic. The
+  :n:`@i_item__i` on the i-th subgoal produced by tactic. The
   execution of tactic should thus generate exactly m subgoals, unless the
   ``[…]`` :token:`i_pattern` comes after an initial ``//`` or ``//=``
   :token:`s_item` that closes some of the goals produced by ``tactic``, in
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2fa4f1fa42..6a0ce20c79 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1281,16 +1281,16 @@ Managing the local context
       is an occurrence clause whose syntax and behavior are described in
       :ref:`goal occurrences <occurrencessets>`.
 
-   .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences }
+   .. tacv:: set (@ident {* @binder } := @term) {? in @goal_occurrences }
 
-      This is equivalent to :n:`set (@ident := fun @binders => @term) {? in @goal_occurrences }`.
+      This is equivalent to :n:`set (@ident := fun {* @binder } => @term) {? in @goal_occurrences }`.
 
    .. tacv:: set @term {? in @goal_occurrences }
 
       This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }`
       but :token:`ident` is generated by Coq.
 
-   .. tacv:: eset (@ident {? @binders } := @term) {? in @goal_occurrences }
+   .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences }
              eset @term {? in @goal_occurrences }
       :name: eset; _
 
@@ -1326,16 +1326,16 @@ Managing the local context
    without performing any replacement in the goal or in the hypotheses. It is
    equivalent to :n:`set (@ident := @term) in |-`.
 
-   .. tacv:: pose (@ident @binders := @term)
+   .. tacv:: pose (@ident {* @binder } := @term)
 
-      This is equivalent to :n:`pose (@ident := fun @binders => @term)`.
+      This is equivalent to :n:`pose (@ident := fun {* @binder } => @term)`.
 
    .. tacv:: pose @term
 
       This behaves as :n:`pose (@ident := @term)` but :token:`ident` is
       generated by Coq.
 
-   .. tacv:: epose (@ident {? @binders} := @term)
+   .. tacv:: epose (@ident {* @binder } := @term)
              epose @term
       :name: epose; _