Convert misc chapters to prodn

4 files changed, 303 insertions, 321 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 37d12e8ce5..5c091f04ac 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -879,7 +879,8 @@ Print/identity tactic: idtac
 .. tacn:: idtac {* {| @ident | @string | @natural } }
    :name: idtac
 
-   Leaves the proof unchanged and prints the given tokens. Strings and integers are printed
+   Leaves the proof unchanged and prints the given tokens. :token:`String<string>`\s
+   and :token:`natural`\s are printed
    literally. If :token:`ident` is an |Ltac| variable, its contents are printed; if not, it
    is an error.
 
@@ -888,7 +889,7 @@ Print/identity tactic: idtac
 Failing
 ~~~~~~~
 
-.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @integer } }
+.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @natural } }
    :name: fail; gfail
 
    :tacn:`fail` is the always-failing tactic: it does not solve any
@@ -919,7 +920,7 @@ Failing
       the call to :tacn:`fail` :n:`@natural` is not enclosed in a :n:`+` construct,
       respecting the algebraic identity.
 
-   :n:`{* {| @ident | @string | @integer } }`
+   :n:`{* {| @ident | @string | @natural } }`
       The given tokens are used for printing the failure message.  If :token:`ident`
       is an |Ltac| variable, its contents are printed; if not, it is an error.
 
@@ -937,7 +938,7 @@ Failing
 
       .. todo the example is too long; could show the Goal True. Proof. once and hide the Aborts
          to shorten it.  And add a line of text before each subexample.  Perhaps add some very short
-         explanations/generalizations (eg gfail always fails; "tac; fail" succeeds but "fail." alone
+         explanations/generalizations (e.g. gfail always fails; "tac; fail" succeeds but "fail." alone
          fails.
 
       .. coqtop:: reset all fail
@@ -1488,7 +1489,7 @@ Examples:
       match_context_rule ::= [ {*, @match_hyp } |- @match_pattern ] => @ltac_expr
       match_hyp ::= | @name := {? [ @match_pattern ] : } @match_pattern
 
-.. todo PR The following items (up to numgoals) are part of "value_tactic".  I'd like to make
+.. todo The following items (up to numgoals) are part of "value_tactic".  I'd like to make
    this a subsection and explain that they all return values.  How do I get a 5th-level section title?
 
 Filling a term context
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 449fc96b5a..b09d6146d8 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -49,7 +49,7 @@ the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
 list of assertion commands is given in :ref:`Assertions`. The command
 :cmd:`Goal` can also be used.
 
-.. cmd:: Goal @form
+.. cmd:: Goal @type
 
    This is intended for quick assertion of statements, without knowing in
    advance which name to give to the assertion, typically for quick
@@ -63,7 +63,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
    This command is available in interactive editing proof mode when the
    proof is completed. Then :cmd:`Qed` extracts a proof term from the proof
    script, switches back to |Coq| top-level and attaches the extracted
-   proof term to the declared name of the original goal. This name is
+   proof term to the declared name of the original goal. The name is
    added to the environment as an opaque constant.
 
    .. exn:: Attempt to save an incomplete proof.
@@ -80,42 +80,42 @@ 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.
 
-.. cmd:: Defined
-
-   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`).
-
 .. cmd:: Save @ident
    :name: Save
 
-   Saves a completed proof with the name :token:`ident`.
+   Saves a completed proof with the name :token:`ident`, which
+   overrides any name provided by the :cmd:`Theorem` command or
+   its variants.
+
+.. cmd:: Defined {? @ident }
+
+   Similar to :cmd:`Qed` and :cmd:`Save`, 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`).  If :token:`ident` is specified,
+   the proof is defined with the given name, which overrides any name
+   provided by the :cmd:`Theorem` command or its variants.
 
 .. cmd:: Admitted
 
    This command is available in interactive editing mode to give up
    the current proof and declare the initial goal as an axiom.
 
-.. cmd:: Abort
+.. cmd:: Abort {? {| All | @ident } }
 
-   This command cancels the current proof development, switching back to
+   Cancels the current proof development, switching back to
    the previous proof development, or to the |Coq| toplevel if no other
-   proof was edited.
-
-   .. exn:: No focused proof (No proof-editing in progress).
-      :undocumented:
+   proof was being edited.
 
-   .. cmdv::  Abort @ident
+   :n:`@ident`
+     Aborts editing the proof named :n:`@ident` for use when you have
+     nested proofs.  See also :flag:`Nested Proofs Allowed`.
 
-      Aborts the editing of the proof named :token:`ident` (in case you have
-      nested proofs).
+   :n:`All`
+     Aborts all current proofs.
 
-      .. seealso:: :flag:`Nested Proofs Allowed`
-
-   .. cmdv:: Abort All
-
-      Aborts all current goals.
+   .. exn:: No focused proof (No proof-editing in progress).
+      :undocumented:
 
 .. cmd:: Proof @term
    :name: Proof `term`
@@ -143,12 +143,26 @@ list of assertion commands is given in :ref:`Assertions`. The command
 
    .. seealso:: :cmd:`Proof with`
 
-.. cmd:: Proof using {+ @ident }
+.. cmd:: Proof using @section_var_expr {? with @ltac_expr }
+
+   .. insertprodn section_var_expr starred_ident_ref
 
-   This command applies in proof editing mode. It declares the set of
+   .. prodn::
+      section_var_expr ::= {* @starred_ident_ref }
+      | {? - } @section_var_expr50
+      section_var_expr50 ::= @section_var_expr0 - @section_var_expr0
+      | @section_var_expr0 + @section_var_expr0
+      | @section_var_expr0
+      section_var_expr0 ::= @starred_ident_ref
+      | ( @section_var_expr ) {? * }
+      starred_ident_ref ::= @ident {? * }
+      | Type {? * }
+      | All
+
+   Opens proof editing mode, declaring the set of
    section variables (see :ref:`gallina-assumptions`) used by the proof.
    At :cmd:`Qed` time, the
-   system will assert that the set of section variables actually used in
+   system verifies that the set of section variables used in
    the proof is a subset of the declared one.
 
    The set of declared variables is closed under type dependency. For
@@ -160,51 +174,30 @@ list of assertion commands is given in :ref:`Assertions`. The command
    the statement. In other words ``Proof using e`` is equivalent to
    ``Proof using Type + e`` for any declaration expression ``e``.
 
-   .. cmdv:: Proof using {+ @ident } with @tactic
-
-      Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`.
-
-      .. seealso:: :ref:`tactics-implicit-automation`
-
-   .. cmdv:: Proof using All
-
-      Use all section variables.
-
-   .. cmdv:: Proof using {? Type }
-
-      Use only section variables occurring in the statement.
-
-   .. cmdv:: Proof using Type*
-
-      The ``*`` operator computes the forward transitive closure. E.g. if the
-      variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type
-      of ``H``. ``Type*`` is the forward transitive closure of the entire set of
-      section variables occurring in the statement.
-
-   .. cmdv:: Proof using -({+ @ident })
-
-      Use all section variables except the list of :token:`ident`.
-
-   .. cmdv:: Proof using @collection__1 + @collection__2
+   :n:`- @section_var_expr50`
+     Use all section variables except those specified by :n:`@section_var_expr50`
 
-      Use section variables from the union of both collections.
-      See :ref:`nameaset` to know how to form a named collection.
+   :n:`@section_var_expr0 + @section_var_expr0`
+     Use section variables from the union of both collections.
+     See :ref:`nameaset` to see how to form a named collection.
 
-   .. cmdv:: Proof using @collection__1 - @collection__2
+   :n:`@section_var_expr0 - @section_var_expr0`
+     Use section variables which are in the first collection but not in the
+     second one.
 
-      Use section variables which are in the first collection but not in the
-      second one.
+   :n:`{? * }`
+     Use the transitive closure of the specified collection.
 
-   .. cmdv:: Proof using @collection - ({+ @ident })
+   :n:`Type`
+     Use only section variables occurring in the statement.  Specifying :n:`*`
+     uses the forward transitive closure of all the section variables occurring
+     in the statement. For example, if the variable ``H`` has type ``p < 5`` then
+     ``H`` is in ``p*`` since ``p`` occurs in the type of ``H``.
 
-      Use section variables which are in the first collection but not in the
-      list of :token:`ident`.
-
-   .. cmdv:: Proof using @collection *
-
-      Use section variables in the forward transitive closure of the collection.
-      The ``*`` operator binds stronger than ``+`` and ``-``.
+   :n:`All`
+     Use all section variables.
 
+   .. seealso:: :ref:`tactics-implicit-automation`
 
 Proof using options
 ```````````````````
@@ -212,10 +205,10 @@ Proof using options
 The following options modify the behavior of ``Proof using``.
 
 
-.. opt:: Default Proof Using "@collection"
+.. opt:: Default Proof Using "@section_var_expr"
    :name: Default Proof Using
 
-   Use :n:`@collection` as the default ``Proof using`` value. E.g. ``Set Default
+   Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default
    Proof Using "a b"`` will complete all ``Proof`` commands not followed by a
    ``using`` part with ``using a b``.
 
@@ -230,7 +223,7 @@ The following options modify the behavior of ``Proof using``.
 Name a set of section hypotheses for ``Proof using``
 ````````````````````````````````````````````````````
 
-.. cmd:: Collection @ident := @collection
+.. cmd:: Collection @ident := @section_var_expr
 
    This can be used to name a set of section
    hypotheses, with the purpose of making ``Proof using`` annotations more
@@ -259,7 +252,7 @@ Name a set of section hypotheses for ``Proof using``
 
 
 
-.. cmd:: Existential @natural := @term
+.. cmd:: Existential @natural {? : @type } := @term
 
    This command instantiates an existential variable. :token:`natural` is an index in
    the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`.
@@ -285,64 +278,60 @@ their own proof modes. The default proof mode used when opening a proof can
 be changed using the following option.
 
 .. opt:: Default Proof Mode @string
-   :name: Default Proof Mode
 
    Select the proof mode to use when starting a proof. Depending on the proof
    mode, various syntactic constructs are allowed when writing an interactive
-   proof. The possible option values are listed below.
-
-   - "Classic": this is the default. It activates the |Ltac| language to interact
-     with the proof, and also allows vernacular commands.
-
-   - "Noedit": this proof mode only allows vernacular commands. No tactic
-     language is activated at all. This is the default when the prelude is not
-     loaded, e.g. through the `-noinit` option for `coqc`.
-
-   - "Ltac2": this proof mode is made available when requiring the Ltac2
-     library, and is set to be the default when it is imported. It allows
-     to use the Ltac2 language, as well as vernacular commands.
-
-   - Some external plugins also define their own proof mode, which can be
-     activated via this command.
+   proof. All proof modes support vernacular commands; the proof mode determines
+   which tactic language and set of tactic definitions are available.  The
+   possible option values are:
+
+   `"Classic"`
+     Activates the |Ltac| language and the tactics with the syntax documented
+     in this manual.
+     Some tactics are not available until the associated plugin is loaded,
+     such as `SSR` or `micromega`.
+     This proof mode is set when the :term:`prelude` is loaded.
+
+   `"Noedit"`
+     No tactic
+     language is activated at all. This is the default when the :term:`prelude`
+     is not loaded, e.g. through the `-noinit` option for `coqc`.
+
+   `"Ltac2"`
+     Activates the Ltac2 language and the Ltac2-specific variants of the documented
+     tactics.
+     This value is only available after :cmd:`Requiring <Require>` Ltac2.
+     :cmd:`Importing <Import>` Ltac2 sets this mode.
+
+   Some external plugins also define their own proof mode, which can be
+   activated with this command.
 
 Navigation in the proof tree
 --------------------------------
 
-.. cmd:: Undo
-
-   This command cancels the effect of the last command. Thus, it
-   backtracks one step.
+.. cmd:: Undo {? {? To } @natural }
 
-.. cmdv:: Undo @natural
+   Cancels the effect of the last :token:`natural` commands or tactics.
+   The :n:`To @natural` form goes back to the specified state number.
+   If :token:`natural` is not specified, the command goes back one command or tactic.
 
-   Repeats Undo :token:`natural` times.
+.. cmd:: Restart
 
-.. cmdv:: Restart
-   :name: Restart
-
-   This command restores the proof editing process to the original goal.
+   Restores the proof editing process to the original goal.
 
    .. exn:: No focused proof to restart.
       :undocumented:
 
-.. cmd:: Focus
+.. cmd:: Focus {? @natural }
 
-   This focuses the attention on the first subgoal to prove and the
+   Focuses the attention on the first subgoal to prove or, if :token:`natural` is
+   specified, the :token:`natural`\-th.  The
    printing of the other subgoals is suspended until the focused subgoal
-   is solved or unfocused. This is useful when there are many current
-   subgoals which clutter your screen.
+   is solved or unfocused.
 
    .. deprecated:: 8.8
 
-      Prefer the use of bullets or focusing brackets (see below).
-
-.. cmdv:: Focus @natural
-
-   This focuses the attention on the :token:`natural` th subgoal to prove.
-
-   .. deprecated:: 8.8
-
-      Prefer the use of focusing brackets with a goal selector (see below).
+      Prefer the use of bullets or focusing brackets with a goal selector (see below).
 
 .. cmd:: Unfocus
 
@@ -361,11 +350,19 @@ Navigation in the proof tree
 .. index:: {
            }
 
-.. cmd:: {| %{ | %} }
+.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket,
+   hence the verbose names
+
+.. tacn:: {? {| @natural | [ @ident ] } : } %{
+         %}
 
-   The command ``{`` (without a terminating period) focuses on the first
-   goal, much like :cmd:`Focus` does, however, the subproof can only be
-   unfocused when it has been fully solved ( *i.e.* when there is no
+   .. todo
+      See https://github.com/coq/coq/issues/12004 and
+      https://github.com/coq/coq/issues/12825.
+
+   ``{`` (without a terminating period) focuses on the first
+   goal.  The subproof can only be
+   unfocused when it has been fully solved (*i.e.*, when there is no
    focused goal left). Unfocusing is then handled by ``}`` (again, without a
    terminating period). See also an example in the next section.
 
@@ -373,67 +370,65 @@ Navigation in the proof tree
    together with a suggestion about the right bullet or ``}`` to unfocus it
    or focus the next one.
 
-   .. cmdv:: @natural: %{
-
-      This focuses on the :token:`natural`\-th subgoal to prove.
+   :n:`@natural:`
+     Focuses on the :token:`natural`\-th subgoal to prove.
 
-   .. cmdv:: [@ident]: %{
+   :n:`[ @ident ]: %{`
+     Focuses on the named goal :token:`ident`.
 
-      This focuses on the named goal :token:`ident`.
-
-      .. note::
+   .. note::
 
-         Goals are just existential variables and existential variables do not
-         get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`.
-         You may also wrap this in an Ltac-definition like:
+      Goals are just existential variables and existential variables do not
+      get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`.
+      You may also wrap this in an Ltac-definition like:
 
-         .. coqtop:: in
+      .. coqtop:: in
 
-            Ltac name_goal name := refine ?[name].
+         Ltac name_goal name := refine ?[name].
 
-      .. seealso:: :ref:`existential-variables`
+   .. seealso:: :ref:`existential-variables`
 
-      .. example::
+   .. example::
 
-         This first example uses the Ltac definition above, and the named goals
-         only serve for documentation.
+      This first example uses the Ltac definition above, and the named goals
+      only serve for documentation.
 
-         .. coqtop:: all
+      .. coqtop:: all
 
-            Goal forall n, n + 0 = n.
-            Proof.
-            induction n; [ name_goal base | name_goal step ].
-            [base]: {
+         Goal forall n, n + 0 = n.
+         Proof.
+         induction n; [ name_goal base | name_goal step ].
+         [base]: {
 
-         .. coqtop:: all
+      .. coqtop:: all
 
-            reflexivity.
+         reflexivity.
 
-         .. coqtop:: in
+      .. coqtop:: in
 
-            }
+         }
 
-         .. coqtop:: all
+      .. coqtop:: all
 
-            [step]: {
+         [step]: {
 
-         .. coqtop:: all
+      .. coqtop:: all
 
-            simpl.
-            f_equal.
-            assumption.
-            }
-            Qed.
+         simpl.
+         f_equal.
+         assumption.
+         }
+         Qed.
 
-         This can also be a way of focusing on a shelved goal, for instance:
+      This can also be a way of focusing on a shelved goal, for instance:
 
-         .. coqtop:: all
+      .. coqtop:: all
 
-            Goal exists n : nat, n = n.
-            eexists ?[x].
-            reflexivity.
-            [x]: exact 0.
-            Qed.
+         Goal exists n : nat, n = n.
+         eexists ?[x].
+         reflexivity.
+         [x]: exact 0.
+         Qed.
 
    .. exn:: This proof is focused, but cannot be unfocused this way.
 
@@ -450,14 +445,14 @@ Navigation in the proof tree
       Brackets are used to focus on a single goal given either by its position
       or by its name if it has one.
 
-  .. seealso:: The error messages about bullets below.
+  .. seealso:: The error messages for bullets below.
 
 .. _bullets:
 
 Bullets
 ```````
 
-Alternatively to ``{`` and ``}``, proofs can be structured with bullets. The
+Alternatively, proofs can be structured with bullets instead of ``{`` and ``}``. The
 use of a bullet ``b`` for the first time focuses on the first goal ``g``, the
 same bullet cannot be used again until the proof of ``g`` is completed,
 then it is mandatory to focus the next goal with ``b``. The consequence is
@@ -552,111 +547,103 @@ Requesting information
 ----------------------
 
 
-.. cmd:: Show
-
-   This command displays the current goals.
-
-   .. exn:: No focused proof.
-      :undocumented:
+.. cmd:: Show {? {| @ident | @natural } }
 
-   .. cmdv:: Show @natural
+   Displays the current goals.
 
-      Displays only the :token:`natural`\-th subgoal.
+   :n:`@natural`
+     Display only the :token:`natural`\-th subgoal.
 
-      .. exn:: No such goal.
-         :undocumented:
+   :n:`@ident`
+     Displays the named goal :token:`ident`. This is useful in
+     particular to display a shelved goal but only works if the
+     corresponding existential variable has been named by the user
+     (see :ref:`existential-variables`) as in the following example.
 
-   .. cmdv:: Show @ident
+     .. example::
 
-      Displays the named goal :token:`ident`. This is useful in
-      particular to display a shelved goal but only works if the
-      corresponding existential variable has been named by the user
-      (see :ref:`existential-variables`) as in the following example.
+        .. coqtop:: all abort
 
-      .. example::
+           Goal exists n, n = 0.
+           eexists ?[n].
+           Show n.
 
-         .. coqtop:: all abort
+   .. exn:: No focused proof.
+      :undocumented:
 
-            Goal exists n, n = 0.
-            eexists ?[n].
-            Show n.
+   .. exn:: No such goal.
+      :undocumented:
 
-   .. cmdv:: Show Proof {? Diffs {? removed } }
-      :name: Show Proof
+.. cmd:: Show Proof {? Diffs {? removed } }
 
-      Displays the proof term generated by the tactics
-      that have been applied so far. If the proof is incomplete, the term
-      will contain holes, which correspond to subterms which are still to be
-      constructed. Each hole is an existential variable, which appears as a
-      question mark followed by an identifier.
+   Displays the proof term generated by the tactics
+   that have been applied so far. If the proof is incomplete, the term
+   will contain holes, which correspond to subterms which are still to be
+   constructed. Each hole is an existential variable, which appears as a
+   question mark followed by an identifier.
 
-      Specifying “Diffs” highlights the difference between the
-      current and previous proof step.  By default, the command shows the
-      output once with additions highlighted.  Including “removed” shows
-      the output twice: once showing removals and once showing additions.
-      It does not examine the :opt:`Diffs` option.  See :ref:`showing_proof_diffs`.
+   Specifying “Diffs” highlights the difference between the
+   current and previous proof step.  By default, the command shows the
+   output once with additions highlighted.  Including “removed” shows
+   the output twice: once showing removals and once showing additions.
+   It does not examine the :opt:`Diffs` option.  See :ref:`showing_proof_diffs`.
 
-   .. cmdv:: Show Conjectures
-      :name: Show Conjectures
+.. cmd:: Show Conjectures
 
-      It prints the list of the names of all the
-      theorems that are currently being proved. As it is possible to start
-      proving a previous lemma during the proof of a theorem, this list may
-      contain several names.
+   Prints the names of all the
+   theorems that are currently being proved. As it is possible to start
+   proving a previous lemma during the proof of a theorem, there may
+   be multiple names.
 
-   .. cmdv:: Show Intro
-      :name: Show Intro
+.. cmd:: Show Intro
 
-      If the current goal begins by at least one product,
-      this command prints the name of the first product, as it would be
-      generated by an anonymous :tacn:`intro`. The aim of this command is to ease
-      the writing of more robust scripts. For example, with an appropriate
-      Proof General macro, it is possible to transform any anonymous :tacn:`intro`
-      into a qualified one such as ``intro y13``. In the case of a non-product
-      goal, it prints nothing.
+   If the current goal begins by at least one product,
+   prints the name of the first product as it would be
+   generated by an anonymous :tacn:`intro`. The aim of this command is to ease
+   the writing of more robust scripts. For example, with an appropriate
+   Proof General macro, it is possible to transform any anonymous :tacn:`intro`
+   into a qualified one such as ``intro y13``. In the case of a non-product
+   goal, it prints nothing.
 
-   .. cmdv:: Show Intros
-      :name: Show Intros
+.. cmd:: Show Intros
 
-      This command is similar to the previous one, it
-      simulates the naming process of an :tacn:`intros`.
+   Similar to the previous command.
+   Simulates the naming process of :tacn:`intros`.
 
-   .. cmdv:: Show Existentials
-      :name: Show Existentials
+.. cmd:: Show Existentials
 
-      Displays all open goals / existential variables in the current proof
-      along with the type and the context of each variable.
+   Displays all open goals / existential variables in the current proof
+   along with the type and the context of each variable.
 
-   .. cmdv:: Show Match @ident
+.. cmd:: Show Match @qualid
 
-      This variant displays a template of the Gallina
-      ``match`` construct with a branch for each constructor of the type
-      :token:`ident`
+   Displays a template of the Gallina :token:`match<term_match>`
+   construct with a branch for each constructor of the type
+   :token:`qualid`.  This is used internally by
+   `company-coq <https://github.com/cpitclaudel/company-coq>`_.
 
-      .. example::
+   .. example::
 
-         .. coqtop:: all
+      .. coqtop:: all
 
-            Show Match nat.
+         Show Match nat.
 
-      .. exn:: Unknown inductive type.
-         :undocumented:
+   .. exn:: Unknown inductive type.
+      :undocumented:
 
-   .. cmdv:: Show Universes
-      :name: Show Universes
+.. cmd:: Show Universes
 
-      It displays the set of all universe constraints and
-      its normalized form at the current stage of the proof, useful for
-      debugging universe inconsistencies.
+   Displays the set of all universe constraints and
+   its normalized form at the current stage of the proof, useful for
+   debugging universe inconsistencies.
 
-   .. cmdv:: Show Goal @natural at @natural
-      :name: Show Goal
+.. cmd:: Show Goal @natural at @natural
 
-      This command is only available in coqtop.  Displays a goal at a
-      proof state using the goal ID number and the proof state ID number.
-      It is primarily for use by tools such as Prooftree that need to fetch
-      goal history in this way.  Prooftree is a tool for visualizing a proof
-      as a tree that runs in Proof General.
+   Available in coqtop.  Displays a goal at a
+   proof state using the goal ID number and the proof state ID number.
+   It is primarily for use by tools such as Prooftree that need to fetch
+   goal history in this way.  Prooftree is a tool for visualizing a proof
+   as a tree that runs in Proof General.
 
 .. cmd:: Guarded
 
@@ -749,7 +736,7 @@ command in |CoqIDE|.  You can change the background colors shown for diffs from
 lets you control other attributes of the highlights, such as the foreground
 color, bold, italic, underline and strikeout.
 
-As of June 2019, Proof General can also display |Coq|-generated proof diffs automatically.
+Proof General can also display |Coq|-generated proof diffs automatically.
 Please see the PG documentation section
 "`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
 for details.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e8938fdd47..fe9a31e220 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -86,42 +86,36 @@ specified, the default selector is used.
    Although other selectors are available, only ``all``, ``!`` or a
    single natural number are valid default goal selectors.
 
-.. _bindingslist:
+.. _bindings:
 
-Bindings list
-~~~~~~~~~~~~~
+Bindings
+~~~~~~~~
 
-Tactics that take a term as an argument may also support a bindings list
+Tactics that take a term as an argument may also accept :token:`bindings`
 to instantiate some parameters of the term by name or position.
-The general form of a term with a bindings list is
-:n:`@term with @bindings_list` where :token:`bindings_list` can take two different forms:
+The general form of a term with :token:`bindings` is
+:n:`@term__tac with @bindings` where :token:`bindings` can take two different forms:
 
-.. _bindings_list_grammar:
+  .. insertprodn bindings bindings
 
   .. prodn::
-     ref ::= @ident
-     | @natural
-     bindings_list ::= {+ (@ref := @term) }
-     | {+ @term }
-
-+ In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an
-  :n:`@ident` or a :n:`@natural`. The references are determined according to the type of
-  :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the
-  type of :n:`@term` and the binding provides the tactic with an instance for the
-  parameter of this name. If :n:`@ref` is a number ``n``, it refers to
-  the ``n``-th non dependent premise of the :n:`@term`, as determined by the type
-  of :n:`@term`.
+     bindings ::= {+ ( {| @ident | @natural } := @term ) }
+     | {+ @one_term }
+
++ In the first form, if an :token:`ident` is specified, it must be bound in the
+  type of :n:`@term` and provides the tactic with an instance for the
+  parameter of this name. If a :token:`natural` is specified, it refers to
+  the ``n``-th non dependent premise of :n:`@term__tac`.
 
   .. exn:: No such binder.
      :undocumented:
 
-+ A bindings list can also be a simple list of terms :n:`{* @term}`.
-  In that case the references to which these terms correspond are
-  determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim`
-  and :tacn:`case`, the terms have to
-  provide instances for all the dependent products in the type of term while in
++ In the second form, the interpretation of the :token:`one_term`\s depend on which
+  tactic they appear in.  For :tacn:`induction`, :tacn:`destruct`, :tacn:`elim`
+  and :tacn:`case`, the :token:`one_term`\s
+  provide instances for all the dependent products in the type of :n:`@term__tac` while in
   the case of :tacn:`apply`, or of :tacn:`constructor` and its variants, only instances
-  for the dependent products that are not bound in the conclusion of the type
+  for the dependent products that are not bound in the conclusion of :n:`@term__tac`
   are required.
 
   .. exn:: Not the right number of missing arguments.
@@ -682,11 +676,11 @@ Applying theorems
       .. exn:: Not the right number of missing arguments.
          :undocumented:
 
-   .. tacv:: apply @term with @bindings_list
+   .. tacv:: apply @term with @bindings
 
       This also provides apply with values for instantiating premises. Here, variables
       are referred by names and non-dependent products by increasing numbers (see
-      :ref:`bindings list <bindingslist>`).
+      :ref:`bindings`).
 
    .. tacv:: apply {+, @term}
 
@@ -747,8 +741,8 @@ Applying theorems
       tactics that backtrack often. Moreover, it does not traverse tuples as :tacn:`apply`
       does.
 
-   .. tacv:: {? simple} apply {+, @term {? with @bindings_list}}
-             {? simple} eapply {+, @term {? with @bindings_list}}
+   .. tacv:: {? simple} apply {+, @term {? with @bindings}}
+             {? simple} eapply {+, @term {? with @bindings}}
       :name: simple apply; simple eapply
 
       This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`.
@@ -888,18 +882,18 @@ Applying theorems
 
       This applies each :token:`term` in sequence in :token:`ident`.
 
-   .. tacv:: apply {+, @term with @bindings_list} in @ident
+   .. tacv:: apply {+, @term with @bindings} in @ident
 
       This does the same but uses the bindings in each :n:`(@ident := @term)` to
       instantiate the parameters of the corresponding type of :token:`term`
-      (see :ref:`bindings list <bindingslist>`).
+      (see :ref:`bindings`).
 
-   .. tacv:: eapply {+, @term {? with @bindings_list } } in @ident
+   .. tacv:: eapply {+, @term {? with @bindings } } in @ident
 
       This works as :tacn:`apply … in` but turns unresolved bindings into
       existential variables, if any, instead of failing.
 
-   .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @simple_intropattern
+   .. tacv:: apply {+, @term {? with @bindings } } in @ident as @simple_intropattern
       :name: apply … in … as
 
       This works as :tacn:`apply … in` then applies the :token:`simple_intropattern`
@@ -911,8 +905,8 @@ Applying theorems
       only on subterms that contain no variables to instantiate and does not
       traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`.
 
-   .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern}
-             {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern}
+   .. tacv:: {? simple} apply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
+             {? simple} eapply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
 
       This summarizes the different syntactic variants of :n:`apply @term in @ident`
       and :n:`eapply @term in @ident`.
@@ -938,48 +932,48 @@ Applying theorems
       :g:`constructor n` where ``n`` is the number of constructors of the head
       of the goal.
 
-   .. tacv:: constructor @natural with @bindings_list
+   .. tacv:: constructor @natural with @bindings
 
       Let ``c`` be the i-th constructor of :g:`I`, then
-      :n:`constructor i with @bindings_list` is equivalent to
-      :n:`intros; apply c with @bindings_list`.
+      :n:`constructor i with @bindings` is equivalent to
+      :n:`intros; apply c with @bindings`.
 
       .. warning::
 
-         The terms in the :token:`bindings_list` are checked in the context
+         The terms in :token:`bindings` are checked in the context
          where constructor is executed and not in the context where :tacn:`apply`
          is executed (the introductions are not taken into account).
 
-   .. tacv:: split {? with @bindings_list }
+   .. tacv:: split {? with @bindings }
       :name: split
 
       This applies only if :g:`I` has a single constructor. It is then
-      equivalent to :n:`constructor 1 {? with @bindings_list }`. It is
+      equivalent to :n:`constructor 1 {? with @bindings }`. It is
       typically used in the case of a conjunction :math:`A \wedge B`.
 
-      .. tacv:: exists @bindings_list
+      .. tacv:: exists @bindings
          :name: exists
 
          This applies only if :g:`I` has a single constructor. It is then equivalent
-         to :n:`intros; constructor 1 with @bindings_list.` It is typically used in
+         to :n:`intros; constructor 1 with @bindings.` It is typically used in
          the case of an existential quantification :math:`\exists x, P(x).`
 
-      .. tacv:: exists {+, @bindings_list }
+      .. tacv:: exists {+, @bindings }
 
-         This iteratively applies :n:`exists @bindings_list`.
+         This iteratively applies :n:`exists @bindings`.
 
       .. exn:: Not an inductive goal with 1 constructor.
          :undocumented:
 
-   .. tacv:: left {? with @bindings_list }
-             right {? with @bindings_list }
+   .. tacv:: left {? with @bindings }
+             right {? with @bindings }
       :name: left; right
 
       These tactics apply only if :g:`I` has two constructors, for
       instance in the case of a disjunction :math:`A \vee B`.
       Then, they are respectively equivalent to
-      :n:`constructor 1 {? with @bindings_list }` and
-      :n:`constructor 2 {? with @bindings_list }`.
+      :n:`constructor 1 {? with @bindings }` and
+      :n:`constructor 2 {? with @bindings }`.
 
       .. exn:: Not an inductive goal with 2 constructors.
          :undocumented:
@@ -1518,13 +1512,13 @@ Controlling the proof flow
    list of remaining subgoal to prove.
 
 .. tacv:: specialize (@ident {* @term}) {? as @simple_intropattern}
-          specialize @ident with @bindings_list {? as @simple_intropattern}
+          specialize @ident with @bindings {? as @simple_intropattern}
    :name: specialize; _
 
    This tactic works on local hypothesis :n:`@ident`. The
    premises of this hypothesis (either universal quantifications or
    non-dependent implications) are instantiated by concrete terms coming either
-   from arguments :n:`{* @term}` or from a :ref:`bindings list <bindingslist>`.
+   from arguments :n:`{* @term}` or from :ref:`bindings`.
    In the first form the application to :n:`{* @term}`  can be partial. The
    first form is equivalent to :n:`assert (@ident := @ident {* @term})`. In the
    second form, instantiation elements can also be partial. In this case the
@@ -1767,7 +1761,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       by :token:`naming_intropattern` (see :tacn:`intros`),
       in particular ``?`` can be used to let |Coq| generate a fresh name.
 
-   .. tacv:: destruct @term with @bindings_list
+   .. tacv:: destruct @term with @bindings
 
       This behaves like :n:`destruct @term` providing explicit instances for
       the dependent premises of the type of :token:`term`.
@@ -1781,9 +1775,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       are left as existential variables to be inferred later, in the same way
       as :tacn:`eapply` does.
 
-   .. tacv:: destruct @term using @term {? with @bindings_list }
+   .. tacv:: destruct @term using @term {? with @bindings }
 
-      This is synonym of :n:`induction @term using @term {? with @bindings_list }`.
+      This is synonym of :n:`induction @term using @term {? with @bindings }`.
 
    .. tacv:: destruct @term in @goal_occurrences
 
@@ -1792,8 +1786,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       clause is an occurrence clause whose syntax and behavior is described
       in :ref:`occurrences sets <occurrencessets>`.
 
-   .. tacv:: destruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
-             edestruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
+   .. tacv:: destruct @term {? with @bindings } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings } } {? in @goal_occurrences }
+             edestruct @term {? with @bindings } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings } } {? in @goal_occurrences }
 
       These are the general forms of :tacn:`destruct` and :tacn:`edestruct`.
       They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``,
@@ -1806,15 +1800,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    recursion. It behaves as :n:`elim @term` but using a case-analysis
    elimination principle and not a recursive one.
 
-.. tacv:: case @term with @bindings_list
+.. tacv:: case @term with @bindings
 
-   Analogous to :n:`elim @term with @bindings_list` above.
+   Analogous to :n:`elim @term with @bindings` above.
 
-.. tacv:: ecase @term {? with @bindings_list }
+.. tacv:: ecase @term {? with @bindings }
    :name: ecase
 
    In case the type of :n:`@term` has dependent premises, or dependent premises
-   whose values are not inferable from the :n:`with @bindings_list` clause,
+   whose values are not inferable from the :n:`with @bindings` clause,
    :n:`ecase` turns them into existential variables to be resolved later on.
 
 .. tacv:: simple destruct @ident
@@ -1906,10 +1900,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    :n:`(p`:sub:`1` :n:`, ... , p`:sub:`n` :n:`)` can be used instead of
    :n:`[ p`:sub:`1` :n:`... p`:sub:`n` :n:`]`.
 
-.. tacv:: induction @term with @bindings_list
+.. tacv:: induction @term with @bindings
 
    This behaves like :tacn:`induction` providing explicit instances for the
-   premises of the type of :n:`term` (see :ref:`bindings list <bindingslist>`).
+   premises of the type of :n:`term` (see :ref:`bindings`).
 
 .. tacv:: einduction @term
    :name: einduction
@@ -1926,7 +1920,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    It does not expect the conclusion of the type of the first :n:`@term` to be
    inductive.
 
-.. tacv:: induction @term using @term with @bindings_list
+.. tacv:: induction @term using @term with @bindings
 
    This behaves as :tacn:`induction … using …` but also providing instances
    for the premises of the type of the second :n:`@term`.
@@ -1954,8 +1948,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
          induction y in x |-   *.
          Show 2.
 
-.. tacv:: induction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences
-          einduction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences
+.. tacv:: induction @term with @bindings as @or_and_intropattern_loc using @term with @bindings in @goal_occurrences
+          einduction @term with @bindings as @or_and_intropattern_loc using @term with @bindings in @goal_occurrences
 
    These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the
    effects of the with, as, using, and in clauses.
@@ -1978,11 +1972,11 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    products, the tactic tries to find an instance for which the elimination
    lemma applies and fails otherwise.
 
-.. tacv:: elim @term with @bindings_list
+.. tacv:: elim @term with @bindings
    :name: elim … with
 
    Allows to give explicit instances to the premises of the type of :n:`@term`
-   (see :ref:`bindings list <bindingslist>`).
+   (see :ref:`bindings`).
 
 .. tacv:: eelim @term
    :name: eelim
@@ -1991,15 +1985,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    existential variables to be resolved later on.
 
 .. tacv:: elim @term using @term
-          elim @term using @term with @bindings_list
+          elim @term using @term with @bindings
 
    Allows the user to give explicitly an induction principle :n:`@term` that
    is not the standard one for the underlying inductive type of :n:`@term`. The
-   :n:`@bindings_list` clause allows instantiating premises of the type of
+   :n:`@bindings` clause allows instantiating premises of the type of
    :n:`@term`.
 
-.. tacv:: elim @term with @bindings_list using @term with @bindings_list
-          eelim @term with @bindings_list using @term with @bindings_list
+.. tacv:: elim @term with @bindings using @term with @bindings
+          eelim @term with @bindings using @term with @bindings
 
    These are the most general forms of :tacn:`elim` and :tacn:`eelim`. It combines the
    effects of the ``using`` clause and of the two uses of the ``with`` clause.
@@ -2148,13 +2142,13 @@ and an explanation of the underlying technique.
    :n:`discriminate @ident` where :n:`@ident` is the identifier for the last
    introduced hypothesis.
 
-.. tacv:: discriminate @term with @bindings_list
+.. tacv:: discriminate @term with @bindings
 
    This does the same thing as :n:`discriminate @term` but using the given
    bindings to instantiate parameters or hypotheses of :n:`@term`.
 
 .. tacv:: ediscriminate @natural
-          ediscriminate @term {? with @bindings_list}
+          ediscriminate @term {? with @bindings}
    :name: ediscriminate; _
 
    This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the
@@ -2212,7 +2206,7 @@ and an explanation of the underlying technique.
    different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and
    :g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and
    :g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable
-   equality has been declared using the command :cmd:`Scheme Equality`
+   equality has been declared using :cmd:`Scheme` :n:`Equality ...`
    (see :ref:`proofschemes-induction-principles`),
    the use of a sigma type is avoided.
 
@@ -2237,13 +2231,13 @@ and an explanation of the underlying technique.
       :n:`injection @ident` where :n:`@ident` is the identifier for the last
       introduced hypothesis.
 
-   .. tacv:: injection @term with @bindings_list
+   .. tacv:: injection @term with @bindings
 
       This does the same as :n:`injection @term` but using the given bindings to
       instantiate parameters or hypotheses of :n:`@term`.
 
    .. tacv:: einjection @natural
-             einjection @term {? with @bindings_list}
+             einjection @term {? with @bindings}
       :name: einjection; _
 
       This works the same as :n:`injection` but if the type of :n:`@term`, or the
@@ -2258,10 +2252,10 @@ and an explanation of the underlying technique.
       .. exn:: goal does not satisfy the expected preconditions.
          :undocumented:
 
-   .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern}
+   .. tacv:: injection @term {? with @bindings} as {+ @simple_intropattern}
              injection @natural as {+ @simple_intropattern}
              injection as {+ @simple_intropattern}
-             einjection @term {? with @bindings_list} as {+ @simple_intropattern}
+             einjection @term {? with @bindings} as {+ @simple_intropattern}
              einjection @natural as {+ @simple_intropattern}
              einjection as {+ @simple_intropattern}
 
@@ -2273,10 +2267,10 @@ and an explanation of the underlying technique.
       to the number of new equalities. The original equality is erased if it
       corresponds to a hypothesis.
 
-   .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern
+   .. tacv:: injection @term {? with @bindings} as @injection_intropattern
              injection @natural as @injection_intropattern
              injection as @injection_intropattern
-             einjection @term {? with @bindings_list} as @injection_intropattern
+             einjection @term {? with @bindings} as @injection_intropattern
              einjection @natural as @injection_intropattern
              einjection as @injection_intropattern
 
@@ -4124,7 +4118,7 @@ use one or several databases specific to your development.
    Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in
    the bases :n:`{+ @ident}`.
 
-.. cmd:: Hint Rewrite {+ @term} using @tactic : {+ @ident}
+.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } }
 
    When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the
    tactic ``tactic`` will be applied to the generated subgoals, the main subgoal
@@ -4600,13 +4594,13 @@ symbol :g:`=`.
    :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last
    introduced hypothesis.
 
-.. tacv:: simplify_eq @term with @bindings_list
+.. tacv:: simplify_eq @term with @bindings
 
    This does the same as :n:`simplify_eq @term` but using the given bindings to
    instantiate parameters or hypotheses of :n:`@term`.
 
 .. tacv:: esimplify_eq @natural
-          esimplify_eq @term {? with @bindings_list}
+          esimplify_eq @term {? with @bindings}
    :name: esimplify_eq; _
 
    This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a684afad09..301559d69d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -980,7 +980,7 @@ described first.
 
    This command has an effect on unfoldable constants, i.e. on constants
    defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command
-   assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc,
+   associated with a definition such as :cmd:`Fixpoint`, etc,
    or by a proof ended by :cmd:`Defined`. The command tells not to unfold the
    constants in the :n:`@reference` sequence in tactics using δ-conversion (unfolding
    a constant is replacing it by its definition).