Convert misc chapters to prodn

24 files changed, 874 insertions, 884 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 1ca85e7e17..96e115fc3d 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -99,10 +99,18 @@ Extraction Options
 Setting the target language
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Extraction Language {| OCaml | Haskell | Scheme | JSON }
+.. cmd:: Extraction Language @language
    :name: Extraction Language
 
-   The ability to fix target language is the first and more important
+   .. insertprodn language language
+
+   .. prodn::
+      language ::= OCaml
+      | Haskell
+      | Scheme
+      | JSON
+
+   The ability to fix target language is the first and most important
    of the extraction options. Default is ``OCaml``.
 
    The JSON output is mostly for development or debugging:
@@ -215,14 +223,15 @@ code elimination performed during extraction, in a way which
 is independent but complementary to the main elimination
 principles of extraction (logical parts and types).
 
-.. cmd:: Extraction Implicit @qualid [ {+ @ident } ]
+.. cmd:: Extraction Implicit @qualid [ {* {| @ident | @integer } } ]
 
-   This experimental command allows declaring some arguments of
-   :token:`qualid` as implicit, i.e. useless in extracted code and hence to
-   be removed by extraction. Here :token:`qualid` can be any function or
-   inductive constructor, and the given :token:`ident` are the names of
-   the concerned arguments. In fact, an argument can also be referred
-   by a number indicating its position, starting from 1.
+   Declares some arguments of
+   :token:`qualid` as implicit, meaning that they are useless in extracted code.
+   The extracted code will omit these arguments.
+   Here :token:`qualid` can be
+   any function or inductive constructor, and the :token:`ident`\s are
+   the names of the useless arguments.  Arguments can can also be
+   identified positionally by :token:`integer`\s starting from 1.
 
 When an actual extraction takes place, an error is normally raised if the
 :cmd:`Extraction Implicit` declarations cannot be honored, that is
@@ -254,12 +263,24 @@ a closed term, and of course the system cannot guess the program which
 realizes an axiom.  Therefore, it is possible to tell the system
 what ML term corresponds to a given axiom. 
 
-.. cmd:: Extract Constant @qualid => @string
+.. cmd:: Extract Constant @qualid {* @string__tv } => {| @ident | @string }
 
    Give an ML extraction for the given constant.
-   The :token:`string` may be an identifier or a quoted string.
 
-.. cmd:: Extract Inlined Constant @qualid => @string
+   :n:`@string__tv`
+     If the type scheme axiom is an arity (a sequence of products followed
+     by a sort), then some type
+     variables have to be given (as quoted strings).
+
+     The number of type variables is checked by the system. For example:
+
+     .. coqtop:: in
+
+        Axiom Y : Set -> Set -> Set.
+        Extract Constant Y "'a" "'b" => " 'a * 'b ".
+
+
+.. cmd:: Extract Inlined Constant @qualid => {| @ident | @string }
 
    Same as the previous one, except that the given ML terms will
    be inlined everywhere instead of being declared via a ``let``.
@@ -282,20 +303,6 @@ what ML term corresponds to a given axiom.
    Extract Constant X => "int".
    Extract Constant x => "0".
 
-Notice that in the case of type scheme axiom (i.e. whose type is an
-arity, that is a sequence of product finished by a sort), then some type
-variables have to be given (as quoted strings). The syntax is then:
-
-.. cmdv:: Extract Constant @qualid {+ @string } => @string
-   :undocumented:
-
-The number of type variables is checked by the system. For example:
-
-.. coqtop:: in
-
-   Axiom Y : Set -> Set -> Set.
-   Extract Constant Y "'a" "'b" => " 'a * 'b ".
-
 Realizing an axiom via :cmd:`Extract Constant` is only useful in the
 case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom
 has no computational content and hence will not appear in extracted
@@ -316,36 +323,35 @@ The system also provides a mechanism to specify ML terms for inductive
 types and constructors. For instance, the user may want to use the ML
 native boolean type instead of the |Coq| one. The syntax is the following:
 
-.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ]
+.. cmd:: Extract Inductive @qualid => {| @ident | @string } [ {* {| @ident | @string } } ] {? @string__match }
 
    Give an ML extraction for the given inductive type. You must specify
-   extractions for the type itself (:n:`@string__1`) and all its
-   constructors (all the :n:`@string` between square brackets). In this form,
+   extractions for the type itself (the initial :n:`{| @ident | @string }`) and all its
+   constructors (the :n:`[ {* {| @ident | @string } } ]`). In this form,
    the ML extraction must be an ML inductive datatype, and the native
    pattern matching of the language will be used.
 
-   When :n:`@string__1` matches the name of the type of characters or strings
+   When the initial :n:`{| @ident | @string }` matches the name of the type of characters or strings
    (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String``
    for Haskell), extraction of literals is handled in a specialized way, so as
    to generate literals in the target language. This feature requires the type
    designated by :n:`@qualid` to be registered as the standard char or string type,
    using the :cmd:`Register` command.
 
-.. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
-
-   Same as before, with a final extra :token:`string` that indicates how to
-   perform pattern matching over this inductive type. In this form,
-   the ML extraction could be an arbitrary type.
-   For an inductive type with :math:`k` constructors, the function used to
-   emulate the pattern matching should expect :math:`k+1` arguments, first the :math:`k`
-   branches in functional form, and then the inductive element to
-   destruct. For instance, the match branch ``| S n => foo`` gives the
-   functional form ``(fun n -> foo)``. Note that a constructor with no
-   arguments is considered to have one unit argument, in order to block
-   early evaluation of the branch: ``| O => bar`` leads to the functional
-   form ``(fun () -> bar)``. For instance, when extracting :g:`nat`
-   into |OCaml| ``int``, the code to be provided has type:
-   ``(unit->'a)->(int->'a)->int->'a``.
+   :n:`@string__match`
+     Indicates how to
+     perform pattern matching over this inductive type. In this form,
+     the ML extraction could be an arbitrary type.
+     For an inductive type with :math:`k` constructors, the function used to
+     emulate the pattern matching should expect :math:`k+1` arguments, first the :math:`k`
+     branches in functional form, and then the inductive element to
+     destruct. For instance, the match branch ``| S n => foo`` gives the
+     functional form ``(fun n -> foo)``. Note that a constructor with no
+     arguments is considered to have one unit argument, in order to block
+     early evaluation of the branch: ``| O => bar`` leads to the functional
+     form ``(fun () -> bar)``. For instance, when extracting :g:`nat`
+     into |OCaml| ``int``, the code to be provided has type:
+     ``(unit->'a)->(int->'a)->int->'a``.
 
 .. caution:: As for :cmd:`Extract Constant`, this command should be used with care:
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index fdc349e0d8..407a38378f 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -170,10 +170,17 @@ compatibility constraints.
 Adding new relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd::  Add Parametric Relation {* @binder } : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
+.. cmd::  Add Parametric Relation {* @binder } : @one_term__A @one_term__Aeq {? reflexivity proved by @one_term } {? symmetry proved by @one_term } {? transitivity proved by @one_term } as @ident
 
-   This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
-   :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.
+   Declares a parametric relation of :n:`@one_term__A`, which is a `Type`, say `T`, with
+   :n:`@one_term__Aeq`, which is a relation on `T`, i.e. of type `(T -> T -> Prop)`.
+   Thus, if :n:`@one_term__A` is
+   :n:`A: forall α__1 … α__n, Type` then :n:`@one_term__Aeq` is
+   :n:`Aeq: forall α__1 … α__n, (A α__1 … α__n) -> (A α__1 … α__n) -> Prop`,
+   or equivalently, :n:`Aeq: forall α__1 … α__n, relation (A α__1 … α__n)`.
+
+   :n:`@one_term__A` and :n:`@one_term__Aeq` must be typeable under the context
+   :token:`binder`\s.  In practice, the :token:`binder`\s usually correspond to the :n:`α`\s
 
    The final :token:`ident` gives a unique name to the morphism and it is used
    by the command to generate fresh names for automatically provided
@@ -189,16 +196,16 @@ Adding new relations and morphisms
    To use this command, you need to first import the module ``Setoid`` using
    the command ``Require Import Setoid``.
 
-.. cmd:: Add Relation
+.. cmd:: Add Relation @one_term @one_term {? reflexivity proved by @one_term } {? symmetry proved by @one_term } {? transitivity proved by @one_term } as @ident
 
-   In case the carrier and relations are not parametric, one can use this command
+   If the carrier and relations are not parametric, use this command
    instead, whose syntax is the same except there is no local context.
 
    The proofs of reflexivity, symmetry and transitivity can be omitted if
    the relation is not an equivalence relation. The proofs must be
    instances of the corresponding relation definitions: e.g. the proof of
    reflexivity must have a type convertible to
-   :g:`reflexive (A t1 ... tn) (Aeq t′ 1 …t′ n)`.
+   :g:`reflexive (A t1 … tn) (Aeq t′ 1 … t′ n)`.
    Each proof may refer to the introduced variables as well.
 
 .. example:: Parametric relation
@@ -219,10 +226,10 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism {* @binder } : (@ident {+ @term__1}) with signature @term__2 as @ident
+.. cmd:: Add Parametric Morphism {* @binder } : @one_term with signature @term as @ident
 
-   This command declares a parametric morphism :n:`@ident {+ @term__1}` of
-   signature :n:`@term__2`.  The final identifier :token:`ident` gives a unique
+   Declares a parametric morphism :n:`@one_term` of
+   signature :n:`@term`.  The final identifier :token:`ident` gives a unique
    name to the morphism and it is used as the base name of the typeclass
    instance definition and as the name of the lemma that proves the
    well-definedness of the morphism. The parameters of the morphism as well as
@@ -525,12 +532,13 @@ counterparts when the relation involved is not Leibniz equality.
 Notice, however, that using the prefixed tactics it is possible to
 pass additional arguments such as ``using relation``.
 
-.. tacv:: setoid_reflexivity
-          setoid_symmetry {? in @ident}
-          setoid_transitivity
-          setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident}
-          setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @ltac_expr3}
-   :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace
+.. tacn:: setoid_reflexivity
+          setoid_symmetry {? in @ident }
+          setoid_transitivity @one_term
+          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @occurrences } {? in @ident }
+          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @occurrences
+          setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 }
+   :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; _; setoid_replace
 
    The ``using relation`` arguments cannot be passed to the unprefixed form.
    The latter argument tells the tactic what parametric relation should
@@ -553,34 +561,35 @@ system up to user defined equalities.
 Printing relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Print Instances
+Use the :cmd:`Print Instances` command with the class names ``Reflexive``, ``Symmetric``
+or ``Transitive`` to print registered reflexive, symmetric or transitive relations and
+with the class name ``Proper`` to print morphisms.
 
-   This command can be used to show the list of currently
-   registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric``
-   or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms
-   (implemented as ``Proper`` instances). When the rewriting tactics refuse
-   to replace a term in a context because the latter is not a composition
-   of morphisms, the :cmd:`Print Instances` command can be useful to understand
-   what additional morphisms should be registered.
+When rewriting tactics refuse
+to replace a term in a context because the latter is not a composition
+of morphisms, this command can be useful to understand
+what additional morphisms should be registered.
 
 .. _deprecated_syntax_for_generalized_rewriting:
 
 Deprecated syntax and backward incompatibilities
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Add Setoid @qualid__1 @qualid__2 @qualid__3 as @ident
+.. cmd:: Add Setoid @one_term__carrier @one_term__congruence @one_term__proofs as @ident
 
    This command for declaring setoids and morphisms is also accepted due
    to backward compatibility reasons.
 
-   Here :n:`@qualid__2` is a congruence relation without parameters, :n:`@qualid__1` is its carrier
-   and :n:`@qualid__3` is an object of type (:n:`Setoid_Theory @qualid__1 @qualid__2`) (i.e. a record
+   Here :n:`@one_term__congruence` is a congruence relation without parameters,
+   :n:`@one_term__carrier` is its carrier and :n:`@one_term__proofs` is an object
+   of type (:n:`Setoid_Theory @one_term__carrier @one_term__congruence`) (i.e. a record
    packing together the reflexivity, symmetry and transitivity lemmas).
    Notice that the syntax is not completely backward compatible since the
    identifier was not required.
 
-.. cmd:: Add Morphism @ident : @ident
-   :name: Add Morphism
+.. cmd:: Add Morphism @one_term : @ident
+         Add Morphism @one_term with signature @term as @ident
+   :name: Add Morphism; _
 
    This command is restricted to the declaration of morphisms
    without parameters. It is not fully backward compatible since the
@@ -590,11 +599,10 @@ Deprecated syntax and backward incompatibilities
    bi-implication in place of a simple implication. In practice, porting
    an old development to the new semantics is usually quite simple.
 
-.. cmd:: Declare Morphism @ident : @ident
+.. cmd:: Declare Morphism @one_term : @ident
    :name: Declare Morphism
 
-   This commands is to be used in a module type to declare a parameter that
-   is a morphism.
+   Declares a parameter in a module type that is a morphism.
 
 Notice that several limitations of the old implementation have been
 lifted. In particular, it is now possible to declare several relations
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index dafa510ade..b81212ad0d 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -125,10 +125,16 @@ term consists of the successive application of its coercions.
 Declaring Coercions
 -------------------------
 
-.. cmd:: Coercion @qualid : @class >-> @class
+.. cmd:: Coercion @reference : @class >-> @class
+         Coercion @ident {? @univ_decl } @def_body
 
-  Declares the construction denoted by :token:`qualid` as a coercion between
-  the two given classes.
+   :name: Coercion; _
+
+  The first form declares the construction denoted by :token:`reference` as a coercion between
+  the two given classes.  The second form defines :token:`ident`
+  just like :cmd:`Definition` :n:`@ident {? @univ_decl } @def_body`
+  and then declares :token:`ident` as a coercion between it source and its target.
+  Both forms support the :attr:`local` attribute, which makes the coercion local to the current section.
 
   .. exn:: @qualid not declared.
      :undocumented:
@@ -174,21 +180,6 @@ Declaring Coercions
      circular. When a new circular coercion path is not convertible with the
      identity function, it will be reported as ambiguous.
 
-  .. cmdv:: Local Coercion @qualid : @class >-> @class
-
-     Declares the construction denoted by :token:`qualid` as a coercion local to
-     the current section.
-
-  .. cmdv:: Coercion @ident := @term {? @type }
-
-     This defines :token:`ident` just like :n:`Definition @ident := term {? @type }`,
-     and then declares :token:`ident` as a coercion between it source and its target.
-
-  .. cmdv:: Local Coercion @ident := @term {? @type }
-
-     This defines :token:`ident` just like :n:`Let @ident := @term  {? @type }`,
-     and then declares :token:`ident` as a coercion between it source and its target.
-
 Some objects can be declared as coercions when they are defined.
 This applies to :ref:`assumptions<gallina-assumptions>` and
 constructors of :ref:`inductive types and record fields<gallina-inductive-definitions>`.
@@ -205,13 +196,11 @@ Use :n:`:>` instead of :n:`:` before the
    function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`,
    and we declare it as an identity coercion between ``C`` and ``D``.
 
+   This command supports the :attr:`local` attribute, which makes the coercion local to the current section.
+
    .. exn:: @class must be a transparent constant.
       :undocumented:
 
-   .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident
-
-      Same as :cmd:`Identity Coercion` but locally to the current section.
-
    .. cmd:: SubClass @ident_decl @def_body
       :name: SubClass
 
@@ -223,9 +212,7 @@ Use :n:`:>` instead of :n:`:` before the
       :n:`Definition @ident := @type.`
       :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`.
 
-   .. cmdv:: Local SubClass @ident_decl @def_body
-
-      Same as before but locally to the current section.
+      This command supports the :attr:`local` attribute, which makes the coercion local to the current section.
 
 
 Displaying Available Coercions
@@ -268,24 +255,15 @@ Classes as Records
 
 .. index:: :> (coercion)
 
-We allow the definition of *Structures with Inheritance* (or classes as records)
-by extending the existing :cmd:`Record` macro. Its new syntax is:
-
-.. cmdv:: {| Record | Structure } {? >} @ident {* @binder } : @sort := {? @ident} { {+; @ident :{? >} @term } }
-
-   The first identifier :token:`ident` is the name of the defined record and
-   :token:`sort` is its type. The optional identifier after ``:=`` is the name
-   of the constructor (it will be :n:`Build_@ident` if not given).
-   The other identifiers are the names of the fields, and :token:`term`
-   are their respective types. If ``:>`` is used instead of ``:`` in
-   the declaration of a field, then the name of this field is automatically
-   declared as a coercion from the record name to the class of this
-   field type. Note that the fields always verify the uniform
-   inheritance condition. If the optional ``>`` is given before the
-   record name, then the constructor name is automatically declared as
-   a coercion from the class of the last field type to the record name
-   (this may fail if the uniform inheritance condition is not
-   satisfied).
+*Structures with Inheritance* may be defined using the :cmd:`Record` command.
+
+Use `>` before the record name to declare the constructor name as
+a coercion from the class of the last field type to the record name
+(this may fail if the uniform inheritance condition is not
+satisfied).  See :token:`record_definition`.
+
+Use `:>` in the field type to declare the field as a coercion from the record name
+to the class of the field type.  See :token:`of_type`.
 
 Coercions and Sections
 ----------------------
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 47589a033d..0942a82d6f 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -25,8 +25,8 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
   ``n`` is an optional integer limiting the proof search depth,
   is an incomplete proof procedure for non-linear arithmetic.
   It is based on John Harrison’s HOL Light
-  driver to the external prover `csdp` [#csdp]_. Note that the `csdp` driver is
-  generating a *proof cache* which makes it possible to rerun scripts
+  driver to the external prover `csdp` [#csdp]_. Note that the `csdp` driver
+  generates a *proof cache* which makes it possible to rerun scripts
   even without `csdp`.
 
 .. flag:: Simplex
@@ -250,7 +250,7 @@ proof by abstracting monomials by variables.
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
 
-.. tacn:: psatz
+.. tacn:: psatz @one_term {? @int_or_var }
    :name: psatz
 
    This tactic explores the *Cone* by increasing degrees – hence the
@@ -300,48 +300,86 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands.
    The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``.
 
-.. cmd:: Add Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } @qualid
+.. cmd:: Add Zify @add_zify @one_term
 
-   This command registers an instance of one of the typeclasses among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``,  ``BinRel``,
-   ``UnOpSpec``, ``BinOpSpec``.
+   .. insertprodn add_zify add_zify
 
-.. cmd:: Show Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec }
+   .. prodn::
+      add_zify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec }
+      | {| PropOp | PropBinOp | PropUOp | Saturate }
+
+   Registers an instance of the specified typeclass.
+
+.. cmd:: Show Zify @show_zify
+
+   .. insertprodn show_zify show_zify
+
+   .. prodn::
+      show_zify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec | Spec }
 
-   The command prints the typeclass instances of one the typeclasses
-   among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``,
-   ``UnOpSpec``, ``BinOpSpec``. For instance, :cmd:`Show Zify` ``InjTyp``
+   Prints instances for the specified typeclass.  For instance, :cmd:`Show Zify` ``InjTyp``
    prints the list of types that supported by :tacn:`zify` i.e.,
    :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
 .. cmd:: Show Zify Spec
 
    .. deprecated:: 8.13
-       Use instead either :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec``.
+       Use :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec`` instead.
+
+.. cmd:: Add InjTyp @one_term
+
+   .. deprecated:: 8.13
+       Use :cmd:`Add Zify` ``InjTyp`` instead.
+
+.. cmd:: Add BinOp @one_term
+
+   .. deprecated:: 8.13
+       Use :cmd:`Add Zify` ``BinOp`` instead.
+
+.. cmd:: Add BinOpSpec @one_term
+
+   .. deprecated:: 8.13
+       Use :cmd:`Add Zify` ``BinOpSpec`` instead.
+
+.. cmd:: Add UnOp @one_term
+
+   .. deprecated:: 8.13
+       Use :cmd:`Add Zify` ``UnOp`` instead.
+
+.. cmd:: Add UnOpSpec @one_term
+
+   .. deprecated:: 8.13
+       Use :cmd:`Add Zify` ``UnOpSpec`` instead.
+
+.. cmd:: Add CstOp @one_term
+
+   .. deprecated:: 8.13
+       Use :cmd:`Add Zify` ``CstOp`` instead.
 
-.. cmd:: Add InjTyp
+.. cmd:: Add BinRel @one_term
 
    .. deprecated:: 8.13
-       Use instead either :cmd:`Add Zify` ``InjTyp``.
+       Use :cmd:`Add Zify` ``BinRel`` instead.
 
-.. cmd:: Add BinOp
+.. cmd:: Add PropOp @one_term
 
    .. deprecated:: 8.13
-       Use instead either :cmd:`Add Zify` ``BinOp``.
+       Use :cmd:`Add Zify` ``PropOp`` instead.
 
-.. cmd:: Add UnOp
+.. cmd:: Add PropBinOp @one_term
 
    .. deprecated:: 8.13
-       Use instead either :cmd:`Add Zify` ``UnOp``.
+       Use :cmd:`Add Zify` ``PropBinOp`` instead.
 
-.. cmd:: Add CstOp
+.. cmd:: Add PropUOp @one_term
 
    .. deprecated:: 8.13
-       Use instead either :cmd:`Add Zify` ``CstOp``.
+       Use :cmd:`Add Zify` ``PropUOp`` instead.
 
-.. cmd:: Add BinRel
+.. cmd:: Add Saturate @one_term
 
    .. deprecated:: 8.13
-       Use instead either :cmd:`Add Zify` ``BinRel``.
+       Use :cmd:`Add Zify` ``Saturate`` instead.
 
 
 
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 0e8660cb0e..3944a34cdc 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -7,10 +7,10 @@ of program refinements. To use the Derive extension it must first be
 required with ``Require Coq.derive.Derive``. When the extension is loaded,
 it provides the following command:
 
-.. cmd:: Derive @ident__1 SuchThat @type As @ident__2
+.. cmd:: Derive @ident__1 SuchThat @one_term As @ident__2
 
-   :n:`@ident__1` can appear in :n:`@type`. This command opens a new proof
-   presenting the user with a goal for :n:`@type` in which the name :n:`@ident__1` is
+   :n:`@ident__1` can appear in :n:`@one_term`. This command opens a new proof
+   presenting the user with a goal for :n:`@one_term` in which the name :n:`@ident__1` is
    bound to an existential variable :g:`?x` (formally, there are other goals
    standing for the existential variables but they are shelved, as
    described in :tacn:`shelve`).
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index 8a64a7ed4b..85e0cb9536 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -5,8 +5,16 @@ Nsatz: tactics for proving equalities in integral domains
 
 :Author: Loïc Pottier
 
-.. tacn:: nsatz
-   :name: nsatz
+
+To use the tactics described in this section, load the ``Nsatz`` module with the
+command ``Require Import Nsatz``.  Alternatively, if you prefer not to transitively depend on the
+files that declare the axioms used to define the real numbers, you can
+``Require Import NsatzTactic`` instead; this will still allow
+:tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`,
+:math:`\mathbb{Q}` and any user-registered rings.
+
+
+.. tacn:: nsatz {? with radicalmax := @one_term strategy := @one_term parameters := @one_term variables := @one_term }
 
    This tactic is for solving goals of the form
 
@@ -32,13 +40,36 @@ Nsatz: tactics for proving equalities in integral domains
 
    doing automatic introductions.
 
-   You can load the ``Nsatz`` module with the command ``Require Import Nsatz``.
+   `radicalmax`
+     bound when searching for r such that
+     :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)`.
+     This argument must be of type `N` (binary natural numbers).
 
-   Alternatively, if you prefer not to transitively depend on the
-   files declaring the axioms used to define the real numbers, you can
-   ``Require Import NsatzTactic`` instead; this will still allow
-   :tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`,
-   :math:`\mathbb{Q}` and any user-registered rings.
+   `strategy`
+     gives the order on variables :math:`X_1,\ldots,X_n` and the strategy
+     used in Buchberger algorithm (see :cite:`sugar` for details):
+
+       * `strategy := 0%Z`: reverse lexicographic order and newest s-polynomial.
+       * `strategy := 1%Z`: reverse lexicographic order and sugar strategy.
+       * `strategy := 2%Z`: pure lexicographic order and newest s-polynomial.
+       * `strategy := 3%Z`: pure lexicographic order and sugar strategy.
+
+   `parameters`
+     a list of parameters of type `R`, containing the variables :math:`X_{i_1},\ldots,X_{i_k}` among
+     :math:`X_1,\ldots,X_n`.  Computation will be performed with
+     rational fractions in these parameters, i.e. polynomials have
+     coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient
+     :math:`c` can be a nonconstant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic
+     produces a goal which states that :math:`c` is not zero.
+
+   `variables`
+     a list of variables of type `R` in the decreasing order in
+     which they will be used in the Buchberger algorithm. If the list is empty,
+     then `lvar` is replaced by all the variables which are not in
+     `parameters`.
+
+   See the file `Nsatz.v <https://github.com/coq/coq/blob/master/test-suite/success/Nsatz.v>`_
+   for examples, especially in geometry.
 
 More about `nsatz`
 ---------------------
@@ -63,32 +94,3 @@ Buchberger algorithm.
 
 This computation is done after a step of *reification*, which is
 performed using :ref:`typeclasses`.
-
-.. tacv:: nsatz with radicalmax:=@natural%N strategy:=@natural%Z parameters:=[{*, @ident}] variables:=[{*, @ident}]
-
-   Most complete syntax for `nsatz`.
-
-   * `radicalmax` is a bound when searching for r such that
-     :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)`
-
-   * `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy
-     used in Buchberger algorithm (see :cite:`sugar` for details):
-
-       * strategy = 0: reverse lexicographic order and newest s-polynomial.
-       * strategy = 1: reverse lexicographic order and sugar strategy.
-       * strategy = 2: pure lexicographic order and newest s-polynomial.
-       * strategy = 3: pure lexicographic order and sugar strategy.
-
-   * `parameters` is the list of variables :math:`X_{i_1},\ldots,X_{i_k}` among
-     :math:`X_1,\ldots,X_n` which are considered as parameters: computation will be performed with
-     rational fractions in these variables, i.e. polynomials are considered
-     with coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient
-     :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic
-     produces a goal which states that :math:`c` is not zero.
-
-   * `variables` is the list of the variables in the decreasing order in
-     which they will be used in the Buchberger algorithm. If `variables` = :g:`(@nil R)`,
-     then `lvar` is replaced by all the variables which are not in
-     `parameters`.
-
-See the test-suite file `Nsatz.v <https://github.com/coq/coq/blob/master/test-suite/success/Nsatz.v>`_ for many examples, especially in geometry.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 0fd66d07db..5da1ac3f46 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -33,7 +33,7 @@ obligations which need to be resolved to create the final term.
 .. _elaborating-programs:
 
 Elaborating programs
----------------------
+--------------------
 
 The main difference from |Coq| is that an object in a type :g:`T : Set` can
 be considered as an object of type :g:`{x : T | P}` for any well-formed
@@ -83,7 +83,7 @@ coercions.
 
 .. flag:: Program Cases
 
-   This controls the special treatment of pattern matching generating equalities
+   Controls the special treatment of pattern matching generating equalities
    and disequalities when using |Program| (it is on by default). All
    pattern-matches and let-patterns are handled using the standard algorithm
    of |Coq| (see :ref:`extendedpatternmatching`) when this flag is
@@ -91,7 +91,7 @@ coercions.
 
 .. flag:: Program Generalized Coercion
 
-   This controls the coercion of general inductive types when using |Program|
+   Controls the coercion of general inductive types when using |Program|
    (the flag is on by default). Coercion of subset types and pairs is still
    active in this case.
 
@@ -104,16 +104,16 @@ coercions.
    typechecking.
 
 .. attr:: program
+   :name: program; Program
 
-   This attribute allows to use the Program mode on a specific
+   Allows using the Program mode on a specific
    definition.  An alternative syntax is to use the legacy ``Program``
-   prefix (cf. :n:`@legacy_attr`) as documented in the rest of this
-   chapter.
+   prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter.
 
 .. _syntactic_control:
 
 Syntactic control over equalities
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 To give more control over the generation of equalities, the
 type checker will fall back directly to |Coq|’s usual typing of dependent
@@ -158,36 +158,20 @@ prove some goals to construct the final definitions.
 Program Definition
 ~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Definition @ident := @term
-
-   This command types the value term in Russell and generates proof
-   obligations. Once solved using the commands shown below, it binds the
-   final |Coq| term to the name :n:`@ident` in the environment.
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Program Definition)
-      :undocumented:
-
-   .. cmdv:: Program Definition @ident : @type := @term
-
-      It interprets the type :n:`@type`, potentially generating proof
-      obligations to be resolved. Once done with them, we have a |Coq|
-      type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq|
-      term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to
-      :n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the
-      set of obligations generated during the interpretation of :n:`@term__0`
-      and the aforementioned coercion derivation are solved.
-
-      .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
-         :undocumented:
+A :cmd:`Definition` command with the :attr:`program` attribute types
+the value term in Russell and generates proof
+obligations. Once solved using the commands shown below, it binds the
+final |Coq| term to the name :n:`@ident` in the environment.
 
-   .. cmdv:: Program Definition @ident {* @binder } : @type := @term
+:n:`Program Definition @ident : @type := @term`
 
-      This is equivalent to:
-
-      :n:`Program Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`.
-
-      .. TODO refer to production in alias
+Interprets the type :n:`@type`, potentially generating proof
+obligations to be resolved. Once done with them, we have a |Coq|
+type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq|
+term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to
+:n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the
+set of obligations generated during the interpretation of :n:`@term__0`
+and the aforementioned coercion derivation are solved.
 
 .. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold`
 
@@ -196,20 +180,8 @@ Program Definition
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @fix_definition {* with @fix_definition }
-
-   The optional :n:`@fixannot` annotation can be one of:
-
-   + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on
-     any subset of the arguments and the optional term
-     :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R`
-     to :g:`lt`.
-
-   + :g:`wf R x` which is equivalent to :g:`measure x R`.
-
-   The structural fixpoint operator behaves just like the one of |Coq| (see
-   :cmd:`Fixpoint`), except it may also generate obligations. It works
-   with mutually recursive definitions too.
+A :cmd:`Fixpoint` command with the :attr:`program` attribute may also generate obligations. It works
+with mutually recursive definitions too.  For example:
 
 .. coqtop:: reset in
 
@@ -223,6 +195,17 @@ Program Fixpoint
      | _ => O
      end.
 
+The :cmd:`Fixpoint` command may include an optional :n:`@fixannot` annotation, which can be:
+
++ :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on
+  any subset of the arguments and the optional term
+  :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R`
+  to :g:`lt`.
+
++ :g:`wf R x` which is equivalent to :g:`measure x R`.
+
+.. todo see https://github.com/coq/coq/pull/12936#discussion_r492747830
+
 Here we have one obligation for each branch (branches for :g:`0` and
 ``(S 0)`` are automatically generated by the pattern matching
 compilation algorithm).
@@ -246,8 +229,6 @@ using the syntax:
      | _ => O
      end.
 
-
-
 .. caution:: When defining structurally recursive functions, the generated
    obligations should have the prototype of the currently defined
    functional in their context. In this case, the obligations should be
@@ -266,67 +247,70 @@ using the syntax:
 Program Lemma
 ~~~~~~~~~~~~~
 
-.. cmd:: Program Lemma @ident : @type
-
-   The Russell language can also be used to type statements of logical
-   properties. It will generate obligations, try to solve them
-   automatically and fail if some unsolved obligations remain. In this
-   case, one can first define the lemma’s statement using :g:`Program
-   Definition` and use it as the goal afterwards. Otherwise the proof
-   will be started with the elaborated version as a goal. The
-   :g:`Program` prefix can similarly be used as a prefix for
-   :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc.
+A :cmd:`Lemma` command with the :attr:`program` attribute uses the Russell
+language to type statements of logical
+properties. It generates obligations, tries to solve them
+automatically and fails if some unsolved obligations remain. In this
+case, one can first define the lemma’s statement using :cmd:`Definition`
+and use it as the goal afterwards. Otherwise the proof
+will be started with the elaborated version as a goal. The
+:attr:`Program` attribute can similarly be used with
+:cmd:`Variable`, :cmd:`Hypothesis`, :cmd:`Axiom` etc.
 
 .. _solving_obligations:
 
 Solving obligations
---------------------
+-------------------
 
 The following commands are available to manipulate obligations. The
 optional identifier is used when multiple functions have unsolved
 obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
-.. cmd:: {? {| Local | Global } } Obligation Tactic := @ltac_expr
+.. cmd:: Obligation Tactic := @ltac_expr
    :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
    automatically, whether to solve them or when starting to prove one,
-   e.g. using :g:`Next`. :g:`Local` makes the setting last only for the current
-   module. Inside sections, local is the default.
+   e.g. using :cmd:`Next Obligation`.
+
+   This command supports the :attr:`local` and :attr:`global` attributes.
+   :attr:`local` makes the setting last only for the current
+   module. :attr:`local` is the default inside sections while :attr:`global`
+   otherwise.
 
 .. cmd:: Show Obligation Tactic
 
    Displays the current default tactic.
 
-.. cmd:: Obligations {? of @ident}
+.. cmd:: Obligations {? of @ident }
 
    Displays all remaining obligations.
 
-.. cmd:: Obligation @natural {? of @ident}
+.. cmd:: Obligation @natural {? of @ident } {? : @type {? with @ltac_expr } }
 
    Start the proof of obligation :token:`natural`.
 
-.. cmd:: Next Obligation {? of @ident}
+.. cmd:: Next Obligation {? of @ident } {? with @ltac_expr }
 
    Start the proof of the next unsolved obligation.
 
-.. cmd:: Solve Obligations {? {? of @ident} with @ltac_expr}
+.. cmd:: Solve Obligations {? of @ident } {? with @ltac_expr }
 
-   Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one.
+   Tries to solve each obligation of :token:`ident` using the given :token:`ltac_expr` or the default one.
 
-.. cmd:: Solve All Obligations {? with @ltac_expr}
+.. cmd:: Solve All Obligations {? with @ltac_expr }
 
    Tries to solve each obligation of every program using the given
    tactic or the default one (useful for mutually recursive definitions).
 
-.. cmd:: Admit Obligations {? of @ident}
+.. cmd:: Admit Obligations {? of @ident }
 
-   Admits all obligations (of ``ident``).
+   Admits all obligations (of :token:`ident`).
 
    .. note:: Does not work with structurally recursive programs.
 
-.. cmd:: Preterm {? of @ident}
+.. cmd:: Preterm {? of @ident }
 
    Shows the term that will be fed to the kernel once the obligations
    are solved. Useful for debugging.
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 9f839364b6..da1a393b4a 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -102,7 +102,7 @@ forget this paragraph and use the tactic according to your intuition.
 Concrete usage in |Coq|
 --------------------------
 
-.. tacn:: ring {? [ {+ @term } ] }
+.. tacn:: ring {? [ {+ @one_term } ] }
 
    Solves polynomical equations of a ring
    (or semiring) structure. It proceeds by normalizing both sides
@@ -110,14 +110,35 @@ Concrete usage in |Coq|
    distributivity, constant propagation, rewriting of monomials) and
    syntactically comparing the results.
 
-.. tacn:: ring_simplify {? [ {+ @term } ] } {+ @term } {? in @ident }
+   :n:`[ {+ @one_term } ]`
+     If specified, the tactic decides the equality of two terms modulo ring operations and
+     the equalities defined by the :token:`one_term`\s.
+     Each :token:`one_term` has to be a proof of some equality :g:`m = p`, where :g:`m`
+     is a monomial (after “abstraction”), :g:`p` a polynomial and :g:`=` is the
+     corresponding equality of the ring structure.
+
+.. tacn:: ring_simplify {? [ {+ @one_term } ] } {+ @one_term } {? in @ident }
 
    Applies the normalization procedure described above to
-   the given terms. The tactic then replaces all occurrences of the terms
-   given in the conclusion of the goal by their normal forms. If no term
+   the given :token:`one_term`\s. The tactic then replaces all occurrences of the :token:`one_term`\s
+   given in the conclusion of the goal by their normal forms. If no :token:`one_term`
    is given, then the conclusion should be an equation and both
    sides are normalized. The tactic can also be applied in a hypothesis.
 
+   :n:`in @ident`
+     If specified, the tactic performs the simplification in the hypothesis named :token:`ident`.
+
+   .. note::
+
+     :n:`ring_simplify @one_term__1; ring_simplify @one_term__2` is not equivalent to
+     :n:`ring_simplify @one_term__1 @one_term__2`.
+
+     In the latter case the variables map is shared between the two :token:`one_term`\s, and
+     common subterm :g:`t` of :n:`@one_term__1` and :n:`@one_term__2`
+     will have the same associated variable number. So the first
+     alternative should be avoided for :token:`one_term`\s belonging to the same ring
+     theory.
+
    The tactic must be loaded by ``Require Import Ring``. The ring structures
    must be declared with the ``Add Ring`` command (see below). The ring of
    booleans is predefined; if one wants to use the tactic on |nat| one must
@@ -147,31 +168,6 @@ Concrete usage in |Coq|
     Abort.
 
 
-.. tacv:: ring [{* @term }] 
- 
-   This tactic decides the equality of two terms modulo ring operations and
-   the equalities defined by the :token:`term`\ s.
-   Each :token:`term` has to be a proof of some equality :g:`m = p`, where :g:`m`
-   is a monomial (after “abstraction”), :g:`p` a polynomial and :g:`=` the
-   corresponding equality of the ring structure.
-
-.. tacv:: ring_simplify [{* @term }] {* @term } in @ident
- 
-   This tactic performs the simplification in the hypothesis named :token:`ident`.
-
-
-.. note:: 
-
-  :n:`ring_simplify @term__1; ring_simplify @term__2` is not equivalent to
-  :n:`ring_simplify @term__1 @term__2`.
-
-  In the latter case the variables map is shared between the two terms, and
-  common subterm :g:`t` of :n:`@term__1` and :n:`@term__2`
-  will have the same associated variable number. So the first
-  alternative should be avoided for terms belonging to the same ring
-  theory.
-
-
 Error messages:
 
 
@@ -515,15 +511,27 @@ application of the main correctness theorem to well-chosen arguments.
 Dealing with fields
 ------------------------
 
-.. tacn:: field {? [ {+ @term } ] }
+.. tacn:: field {? [ {+ @one_term } ] }
 
-   This tactic is an extension of the :tacn:`ring` tactic that deals with rational
+   An extension of the :tacn:`ring` tactic that deals with rational
    expressions. Given a rational expression :math:`F = 0`. It first reduces the
    expression `F` to a common denominator :math:`N/D = 0` where `N` and `D`
    are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this
    gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve
    :math:`N = 0`.
 
+   :n:`[ {+ @one_term } ]`
+     If specified, the tactic decides the equality of two terms modulo
+     field operations and the equalities defined
+     by the :token:`one_term`\s. Each :token:`one_term` has to be a proof of some equality
+     :g:`m = p`, where :g:`m` is a monomial (after “abstraction”), :g:`p` a polynomial
+     and :g:`=` the corresponding equality of the field structure.
+
+  .. note::
+
+     Rewriting works with the equality  :g:`m = p` only if :g:`p` is a polynomial since
+     rewriting is handled by the underlying ring tactic.
+
    Note that :n:`field` also generates nonzero conditions for all the
    denominators it encounters in the reduction. In our example, it
    generates the condition :math:`x \neq 0`. These conditions appear as one subgoal
@@ -559,71 +567,36 @@ Dealing with fields
     intros x y H H1; field [H1]; auto.
     Abort.
 
-.. tacv:: field [{* @term}] 
-
-   This tactic decides the equality of two terms modulo
-   field operations and the equalities defined
-   by the :token:`term`\s. Each :token:`term` has to be a proof of some equality
-   :g:`m = p`, where :g:`m` is a monomial (after “abstraction”), :g:`p` a polynomial
-   and :g:`=` the corresponding equality of the field structure.
-
-.. note:: 
-
-   Rewriting works with the equality  :g:`m = p` only if :g:`p` is a polynomial since
-   rewriting is handled by the underlying ring tactic.
-
-.. tacn:: field_simplify {? [ {+ @term } ] } {+ @term } {? in @ident }
+.. tacn:: field_simplify {? [ {+ @one_term__eq } ] } {+ @one_term } {? in @ident }
  
-   performs the simplification in the conclusion of the
+   Performs the simplification in the conclusion of the
    goal, :math:`F_1 = F_2` becomes :math:`N_1 / D_1 = N_2 / D_2`. A normalization step
    (the same as the one for rings) is then applied to :math:`N_1`, :math:`D_1`, 
    :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during
    fraction simplification. This yields smaller expressions when
    reducing to the same denominator since common factors can be canceled.
 
-.. tacv:: field_simplify [{* @term }] 
-
-   This variant performs the simplification in the conclusion of the goal using the equalities
-   defined by the :token:`term`\s.
-
-.. tacv:: field_simplify [{* @term }] {* @term }
-
-   This variant performs the simplification in the terms :token:`term`\s  of the conclusion of the goal
-   using the equalities defined by :token:`term`\s inside the brackets.
-
-.. tacv:: field_simplify in @ident
-
-   This variant performs the simplification in the assumption :token:`ident`.
-
-.. tacv:: field_simplify [{* @term }] in @ident
- 
-   This variant performs the simplification
-   in the assumption :token:`ident` using the equalities defined by the :token:`term`\s.
-
-.. tacv:: field_simplify [{* @term }] {* @term } in @ident
-
-   This variant performs the simplification in the :token:`term`\s of the
-   assumption :token:`ident` using the
-   equalities defined by the :token:`term`\s inside the brackets.
-
-.. tacn:: field_simplify_eq {? [ {+ @term } ] } {? in @ident }
-
-   performs the simplification in the conclusion of
-   the goal removing the denominator. :math:`F_1 = F_2` becomes :math:`N_1 D_2 = N_2 D_1`.
+   :n:`[ {+ @one_term__eq } ]`
+     Do simplification in the conclusion of the goal using the equalities
+     defined by these :token:`one_term`\s.
 
-.. tacv:: field_simplify_eq [ {* @term }]
+   :n:`{+ @one_term }`
+     Terms to simplify in the conclusion.
 
-   This variant performs the simplification in
-   the conclusion of the goal using the equalities defined by :token:`term`\s.
+   :n:`in @ident`
+     If specified, substitute in the hypothesis :n:`@ident` instead of the conclusion.
 
-.. tacv:: field_simplify_eq in @ident
+.. tacn:: field_simplify_eq {? [ {+ @one_term } ] } {? in @ident }
 
-   This variant performs the simplification in the assumption :token:`ident`.
+   Performs the simplification in the conclusion of
+   the goal, removing the denominator. :math:`F_1 = F_2` becomes :math:`N_1 D_2 = N_2 D_1`.
 
-.. tacv:: field_simplify_eq [{* @term}] in @ident
+   :n:`[ {+ @one_term } ]`
+     Do simplification in the conclusion of the goal using the equalities
+     defined by these :token:`one_term`\s.
 
-   This variant performs the simplification in the assumption :token:`ident`
-   using the equalities defined by :token:`term`\s and removing the denominator.
+   :n:`in @ident`
+     If specified, simplify in the hypothesis :n:`@ident` instead of the conclusion.
 
 
 Adding a new field structure
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 8cbc436ab7..7638fce010 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -295,10 +295,29 @@ the Existing Instance command to achieve the same effect.
 Summary of the commands
 -----------------------
 
-.. cmd:: Class @inductive_definition {* with @inductive_definition }
+.. cmd:: Class @record_definition
+         Class @singleton_class_definition
 
-   The :cmd:`Class` command is used to declare a typeclass with parameters
-   :n:`{* @binder }` and fields the declared record fields.
+   .. insertprodn singleton_class_definition singleton_class_definition
+
+   .. prodn::
+      singleton_class_definition ::= {? > } @ident_decl {* @binder } {? : @sort } := @constructor
+
+   The first form declares a record and makes the record a typeclass with parameters
+   :n:`{* @binder }` and the listed record fields.
+
+   .. _singleton-class:
+
+   The second form declares a *singleton* class with a single method.  This
+   singleton class is a so-called definitional class, represented simply
+   as a definition ``ident binders := term`` and whose instances are
+   themselves objects of this type. Definitional classes are not wrapped
+   inside records, and the trivial projection of an instance of such a
+   class is convertible to the instance itself. This can be useful to
+   make instances of existing objects easily and to reduce proof size by
+   not inserting useless projections. The class constant itself is
+   declared rigid during resolution so that the class abstraction is
+   maintained.
 
    Like any command declaring a record, this command supports the
    :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
@@ -306,22 +325,7 @@ Summary of the commands
    :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and
    :attr:`private(matching)` attributes.
 
-   .. _singleton-class:
-
-   .. cmdv:: Class @ident {* @binder } : {? @sort} := @ident : @term
-
-      This variant declares a *singleton* class with a single method.  This
-      singleton class is a so-called definitional class, represented simply
-      as a definition ``ident binders := term`` and whose instances are
-      themselves objects of this type. Definitional classes are not wrapped
-      inside records, and the trivial projection of an instance of such a
-      class is convertible to the instance itself. This can be useful to
-      make instances of existing objects easily and to reduce proof size by
-      not inserting useless projections. The class constant itself is
-      declared rigid during resolution so that the class abstraction is
-      maintained.
-
-   .. cmdv:: Existing Class @ident
+   .. cmd:: Existing Class @qualid
 
       This variant declares a class from a previously declared constant or
       inductive definition. No methods or instances are defined.
@@ -330,27 +334,31 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @natural} := { {*; @field_def} }
+.. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } }
+
+   .. insertprodn hint_info hint_info
 
-   This command is used to declare a typeclass instance named
-   :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
+   .. prodn::
+      hint_info ::= %| {? @natural } {? @one_term }
+
+   Declares a typeclass instance named
+   :token:`ident_decl` of the class :n:`@type` with the specified parameters and with
    fields defined by :token:`field_def`, where each field must be a declared field of
    the class.
 
-   An arbitrary context of :n:`{* @binder }` can be put after the name of the
-   instance and before the colon to declare a parameterized instance. An
-   optional priority can be declared, 0 being the highest priority as for
-   :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number
+   Add one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info`
+   specifies the hint priority, where 0 is the highest priority as for
+   :tacn:`auto` hints. If the priority is not specified, the default is the number
    of non-dependent binders of the instance.
 
    This command supports the :attr:`global` attribute that can be
    used on instances declared in a section so that their
-   generalization is automatically redeclared after the section is
+   generalization is automatically redeclared when the section is
    closed.
 
    Like :cmd:`Definition`, it also supports the :attr:`program`
    attribute to switch the type checking to `Program` (chapter
-   :ref:`programs`) and use the obligation mechanism to manage missing
+   :ref:`programs`) and to use the obligation mechanism to manage missing
    fields.
 
    Finally, it supports the lighter :attr:`refine` attribute:
@@ -362,67 +370,43 @@ Summary of the commands
       to fill them.  It works exactly as if no body had been given and
       the :tacn:`refine` tactic has been used first.
 
-   .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @natural } := @term
-
-      This syntax is used for declaration of singleton class instances or
-      for directly giving an explicit term of type :n:`forall {* @binder }, @term__0
-      {+ @term}`.  One need not even mention the unique field name for
-      singleton classes.
-
-   .. cmdv:: Declare Instance
-      :name: Declare Instance
+   .. cmd:: Declare Instance @ident_decl {* @binder } : @term {? @hint_info }
 
-      In a :cmd:`Module Type`, this command states that a corresponding concrete
+      In a :cmd:`Module Type`, declares that a corresponding concrete
       instance should exist in any implementation of this :cmd:`Module Type`. This
       is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or
       between :cmd:`Declare Module` and :cmd:`Module`.
 
 
-Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
-few other commands related to typeclasses.
+   .. cmd:: Existing Instance @qualid {? @hint_info }
+            Existing Instances {+ @qualid } {? %| @natural }
+
+      Adds a constant whose type ends with
+      an applied typeclass to the instance database with an optional
+      priority :token:`natural`.  It can be used for redeclaring instances at the end of
+      sections, or declaring structure projections as instances. This is
+      equivalent to ``Hint Resolve ident : typeclass_instances``, except it
+      registers instances for :cmd:`Print Instances`.
+
+.. cmd:: Print Instances @reference
 
-.. cmd:: Existing Instance {+ @ident} {? | @natural}
+   Shows the list of instances associated with the typeclass :token:`reference`.
 
-   This command adds an arbitrary list of constants whose type ends with
-   an applied typeclass to the instance database with an optional
-   priority :token:`natural`.  It can be used for redeclaring instances at the end of
-   sections, or declaring structure projections as instances. This is
-   equivalent to ``Hint Resolve ident : typeclass_instances``, except it
-   registers instances for :cmd:`Print Instances`.
 
-.. tacn:: typeclasses eauto
-   :name: typeclasses eauto
+.. tacn:: typeclasses eauto {? bfs } {? @int_or_var } {? with {+ @ident } }
 
-   This proof search tactic implements the resolution engine that is run
+   This proof search tactic uses the resolution engine that is run
    implicitly during type checking. This tactic uses a different resolution
    engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the
    following:
 
-   + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in
-     the new proof engine (as of Coq 8.6), meaning that backtracking is
+   + Unlike :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in
+     the proof engine, meaning that backtracking is
      available among dependent subgoals, and shelving goals is supported.
      ``typeclasses eauto`` is a multi-goal tactic. It analyses the dependencies
      between subgoals to avoid backtracking on subgoals that are entirely
      independent.
 
-   + When called with no arguments, ``typeclasses eauto`` uses
-     the ``typeclass_instances`` database by default (instead of core).
-     Dependent subgoals are automatically shelved, and shelved goals can
-     remain after resolution ends (following the behavior of Coq 8.5).
-
-     .. note::
-        As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully
-        mimics what happens during typeclass resolution when it is called
-        during refinement/type inference, except that *only* declared class
-        subgoals are considered at the start of resolution during type
-        inference, while ``all`` can select non-class subgoals as well. It might
-        move to ``all:typeclasses eauto`` in future versions when the
-        refinement engine will be able to backtrack.
-
-   + When called with specific databases (e.g. with), ``typeclasses eauto``
-     allows shelved goals to remain at any point during search and treat
-     typeclass goals like any other.
-
    + The transparency information of databases is used consistently for
      all hints declared in them. It is always used when calling the
      unifier. When considering local hypotheses, we use the transparent
@@ -446,26 +430,44 @@ few other commands related to typeclasses.
    + When considering local hypotheses, we use the union of all the modes
      declared in the given databases.
 
-   .. tacv:: typeclasses eauto @natural
+   + Use the :cmd:`Typeclasses eauto` command to customize the behavior of
+     this tactic.
 
-      .. warning::
-         The semantics for the limit :n:`@natural`
-         is different than for auto. By default, if no limit is given, the
-         search is unbounded. Contrary to :tacn:`auto`, introduction steps are
-         counted, which might result in larger limits being necessary when
-         searching with ``typeclasses eauto`` than with :tacn:`auto`.
+   :n:`@int_or_var`
+     Specifies the maximum depth of the search.
 
-   .. tacv:: typeclasses eauto with {+ @ident}
+      .. warning::
+         The semantics for the limit :n:`@int_or_var`
+         are different than for :tacn:`auto`. By default, if no limit is given, the
+         search is unbounded. Unlike :tacn:`auto`, introduction steps count against
+         the limit, which might result in larger limits being necessary when
+         searching with :tacn:`typeclasses eauto` than with :tacn:`auto`.
+
+   :n:`with {+ @ident }`
+     Runs resolution with the specified hint databases. It treats
+     typeclass subgoals the same as other subgoals (no shelving of
+     non-typeclass goals in particular), while allowing shelved goals
+     to remain at any point during search.
+
+     When :n:`with` is not specified, :tacn:`typeclasses eauto` uses
+     the ``typeclass_instances`` database by default (instead of ``core``).
+     Dependent subgoals are automatically shelved, and shelved goals can
+     remain after resolution ends (following the behavior of Coq 8.5).
 
-      This variant runs resolution with the given hint databases. It treats
-      typeclass subgoals the same as other subgoals (no shelving of
-      non-typeclass goals in particular).
+     .. note::
+        ``all:once (typeclasses eauto)`` faithfully
+        mimics what happens during typeclass resolution when it is called
+        during refinement/type inference, except that *only* declared class
+        subgoals are considered at the start of resolution during type
+        inference, while ``all`` can select non-class subgoals as well. It might
+        move to ``all:typeclasses eauto`` in future versions when the
+        refinement engine will be able to backtrack.
 
-.. tacn:: autoapply @term with @ident
+.. tacn:: autoapply @one_term with @ident
    :name: autoapply
 
-   The tactic ``autoapply`` applies a term using the transparency information
-   of the hint database ident, and does *no* typeclass resolution. This can
+   The tactic ``autoapply`` applies :token:`one_term` using the transparency information
+   of the hint database :token:`ident`, and does *no* typeclass resolution. This can
    be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint
    database ``typeclass_instances``) to allow backtracking on the typeclass
    subgoals created by the lemma application, rather than doing typeclass
@@ -476,16 +478,16 @@ few other commands related to typeclasses.
 Typeclasses Transparent, Typeclasses Opaque
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses Transparent {+ @ident}
+.. cmd:: Typeclasses Transparent {+ @qualid }
 
-   This command makes the identifiers transparent during typeclass
+   Makes :token:`qualid` transparent during typeclass
    resolution.
-   Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`.
+   A shortcut for :cmd:`Hint Transparent` :n:`{+ @qualid } : typeclass_instances`
 
-.. cmd:: Typeclasses Opaque {+ @ident}
+.. cmd:: Typeclasses Opaque {+ @qualid }
 
-   Make the identifiers opaque for typeclass search.
-   Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`.
+   Make :token:`qualid` opaque for typeclass search.
+   A shortcut for :cmd:`Hint Opaque` :n:`{+ @qualid } : typeclass_instances`.
 
    It is useful when some constants prevent some unifications and make
    resolution fail. It is also useful to declare constants which
@@ -517,7 +519,7 @@ Settings
 
 .. flag:: Typeclasses Filtered Unification
 
-   This flag, available since |Coq| 8.6 and off by default, switches the
+   This flag, which is off by default, switches the
    hint application procedure to a filter-then-unify strategy. To apply a
    hint, we first check that the goal *matches* syntactically the
    inferred or specified pattern of the hint, and only then try to
@@ -601,22 +603,25 @@ Settings
    of goals.  Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this
    option to 0 turns that flag off.
 
-Typeclasses eauto `:=`
-~~~~~~~~~~~~~~~~~~~~~~
+Typeclasses eauto
+~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @natural
+.. cmd:: Typeclasses eauto := {? debug } {? ( {| bfs | dfs } ) } {? @natural }
    :name: Typeclasses eauto
 
-   This command allows more global customization of the typeclass
-   resolution tactic. The semantics of the options are:
+   Allows more global customization of the :tacn:`typeclasses eauto` tactic.
+   The options are:
 
-   + ``debug`` This sets the debug mode. In debug mode, the trace of
-     successfully applied tactics is printed. The debug mode can also
+   ``debug``
+     Sets debug mode. In debug mode, a trace of
+     successfully applied tactics is printed. Debug mode can also
      be set with :flag:`Typeclasses Debug`.
 
-   + ``(dfs)``, ``(bfs)`` This sets the search strategy to depth-first
+   ``dfs``, ``bfs``
+     Sets the search strategy to depth-first
      search (the default) or breadth-first search. The search strategy
      can also be set with :flag:`Typeclasses Iterative Deepening`.
 
-   + :token:`natural` This sets the depth limit of the search. The depth
-     limit can also be set with :opt:`Typeclasses Depth`.
+   :token:`natural`
+     Sets the depth limit for the search. The limit can also be set with
+     :opt:`Typeclasses Depth`.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index b0ef792bd1..dd26534ec7 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -123,6 +123,7 @@ Polymorphic, Monomorphic
 -------------------------
 
 .. attr:: universes(polymorphic)
+   :name: universes(polymorphic); Polymorphic
 
    This attribute can be used to declare universe polymorphic
    definitions and inductive types.  There is also a legacy syntax
@@ -136,6 +137,7 @@ Polymorphic, Monomorphic
    used.
 
 .. attr:: universes(monomorphic)
+   :name: universes(monomorphic); Monomorphic
 
    This attribute can be used to declare universe monomorphic
    definitions and inductive types (i.e. global universe constraints
@@ -170,6 +172,7 @@ Cumulative, NonCumulative
 -------------------------
 
 .. attr:: universes(cumulative)
+   :name: universes(cumulative); Cumulative
 
    Polymorphic inductive types, coinductive types, variants and
    records can be declared cumulative using this attribute or the
@@ -200,6 +203,7 @@ Cumulative, NonCumulative
    effect on *monomorphic* inductive definitions.
 
 .. attr:: universes(noncumulative)
+   :name: universes(noncumulative); NonCumulative
 
    Declares the inductive type as non-cumulative even if the
    :flag:`Polymorphic Inductive Cumulativity` flag is on.  There is
@@ -384,29 +388,26 @@ Explicit Universes
 The syntax has been extended to allow users to explicitly bind names
 to universes and explicitly instantiate polymorphic definitions.
 
-.. cmd:: Universe @ident
-         Polymorphic Universe @ident
+.. cmd:: Universe {+ @ident }
 
-   In the monorphic case, this command declares a new global universe
-   named :token:`ident`, which can be referred to using its qualified name
-   as well. Global universe names live in a separate namespace. The
-   command supports the :attr:`universes(polymorphic)` attribute (or
-   the ``Polymorphic`` prefix) only in sections, meaning the universe
-   quantification will be discharged on each section definition
+   In the monomorphic case, declares new global universes
+   with the given names.  Global universe names live in a separate namespace.
+   The command supports the :attr:`universes(polymorphic)` attribute (or
+   the ``Polymorphic`` legacy attribute) only in sections, meaning the universe
+   quantification will be discharged for each section definition
    independently.
 
    .. exn:: Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead.
       :undocumented:
 
-.. cmd:: Constraint @univ_constraint
-         Polymorphic Constraint @univ_constraint
+.. cmd:: Constraint {+, @univ_constraint }
 
-   This command declares a new constraint between named universes.
+   Declares new constraints between named universes.
 
-   If consistent, the constraint is then enforced in the global
+   If consistent, the constraints are then enforced in the global
    environment. Like :cmd:`Universe`, it can be used with the
    :attr:`universes(polymorphic)` attribute (or the ``Polymorphic``
-   prefix) in sections only to declare constraints discharged at
+   legacy attribute) in sections only to declare constraints discharged at
    section closing time. One cannot declare a global constraint on
    polymorphic universes.
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index a8a574c861..75ac2a76cd 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,9 +183,7 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
-    'collection',
     'tactic',
-    'bindings',
     'induction_clause',
     'conversion',
     'where',
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 6cdc272fd4..a38282d41a 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -141,8 +141,8 @@ has type :n:`@type`.
       of_type ::= {| : | :> } @type
 
    These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
-   the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence
-   of an object of this type) is accepted as a postulate.
+   the global context. The fact asserted by :n:`@type` (or, equivalently, the existence
+   of an object of this type) is accepted as a postulate.  They accept the :attr:`program` attribute.
 
    :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
    are equivalent.  They can take the :attr:`local` :term:`attribute`,
@@ -155,6 +155,10 @@ has type :n:`@type`.
    is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly
    parameterized (i.e., the variables are *discharged*).  See Section :ref:`section-mechanism`.
 
+   :n:`:>`
+     If specified, :token:`ident_decl` is automatically
+     declared as a coercion to the class of its type.  See :ref:`coercions`.
+
    The :n:`Inline` clause is only relevant inside functors.  See :cmd:`Module`.
 
 .. example:: Simple assumptions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 3cc3fe231a..321199f05f 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -325,10 +325,10 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
      boldface label "Command:".  Commands are listed in the
      :ref:`command_index`.  Example:
 
-     .. cmd:: Comments {* @string }
+     .. cmd:: Comments {* {| @one_term | @string | @natural } }
 
-        This command prints "Comments ok" and does not change anything
-        to the state of the document.
+        Prints "Comments ok" and does not change
+        the state of the document.
 
    tactic
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 592b16a72f..8d67a3cf40 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -87,7 +87,7 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`program` and
+   :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`) and
    :attr:`canonical` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
@@ -140,6 +140,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and
    the theorem is bound to the name :n:`@ident` in the environment.
 
+   These commands accept the :attr:`program` attribute.  See :ref:`program_lemma`.
+
    Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction
    over a mutually inductive assumption, or that assert mutually dependent
    statements in some mutual co-inductive type. It is equivalent to
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 0b18c9dcf1..122b0f5dfb 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -361,7 +361,11 @@ syntax: :n:`let fix @ident {* @binder } := @term in` stands for
 
 Some options of :n:`@fixannot` are only supported in specific constructs.  :n:`fix` and :n:`let fix`
 only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in
-commands such as :cmd:`Function` and :cmd:`Program Fixpoint`.
+commands such as :cmd:`Fixpoint` (with the :attr:`program` attribute) and :cmd:`Function`.
+
+.. todo explanation of struct: see text above at the Fixpoint command, also
+   see https://github.com/coq/coq/pull/12936#discussion_r510716268 and above.
+   Consider whether to move the grammar for fixannot elsewhere
 
 .. _Fixpoint:
 
@@ -379,7 +383,7 @@ constructions.
    .. prodn::
       fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations }
 
-   This command allows defining functions by pattern matching over inductive
+   Allows defining functions by pattern matching over inductive
    objects using a fixed point construction. The meaning of this declaration is
    to define :n:`@ident` as a recursive function with arguments specified by
    the :n:`@binder`\s such that :n:`@ident` applied to arguments
@@ -388,6 +392,8 @@ constructions.
    consequently :n:`forall {* @binder }, @type` and its value is equivalent
    to :n:`fun {* @binder } => @term`.
 
+   This command accepts the :attr:`program` attribute.
+
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
    are needed to ensure that the :cmd:`Fixpoint` definition always terminates.
@@ -399,7 +405,7 @@ constructions.
    that satisfies the decreasing condition.
 
    :cmd:`Fixpoint` without the :attr:`program` attribute does not support the
-   :n:`wf` or :n:`measure` clauses of :n:`@fixannot`.
+   :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`.
 
    The :n:`with` clause allows simultaneously defining several mutual fixpoints.
    It is especially useful when defining functions over mutually defined
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index b2099b8636..e6df3ee9f5 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -18,7 +18,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
    .. insertprodn record_definition field_def
 
    .. prodn::
-      record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations }
+      record_definition ::= {? > } @ident_decl {* @binder } {? : @sort } {? := {? @ident } %{ {*; @record_field } {? ; } %} }
       record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations }
       field_body ::= {* @binder } @of_type
       | {* @binder } @of_type := @term
@@ -26,19 +26,28 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
       term_record ::= %{%| {*; @field_def } {? ; } %|%}
       field_def ::= @qualid {* @binder } := @term
 
-
    Each :n:`@record_definition` defines a record named by :n:`@ident_decl`.
    The constructor name is given by :n:`@ident`.
    If the constructor name is not specified, then the default name :n:`Build_@ident` is used,
    where :n:`@ident` is the record name.
 
-   If :n:`@type` is
-   omitted, the default type is :math:`\Type`. The identifiers inside the brackets are the field names.
-   The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`.
+   If :token:`sort` is omitted, the default sort is Type.
    Notice that the type of an identifier can depend on a previously-given identifier. Thus the
    order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole
    or to individual fields.
 
+   .. todo
+      "Record foo2:Prop := { a }." gives the error "Cannot infer this placeholder of type "Type",
+      while "Record foo2:Prop := { a:Type }." gives the output "foo2 is defined.
+      a cannot be defined because it is informative and foo2 is not."
+      Your thoughts?
+
+   :n:`{? > }`
+     If provided, the constructor name is automatically declared as
+     a coercion from the class of the last field type to the record name
+     (this may fail if the uniform inheritance condition is not
+     satisfied).  See :ref:`coercions`.
+
    Notations can be attached to fields using the :n:`@decl_notations` annotation.
 
    :cmd:`Record` and :cmd:`Structure` are synonyms.
@@ -76,7 +85,7 @@ Let us now see the work done by the ``Record`` macro. First the macro
 generates a variant type definition with just one constructor:
 :n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`.
 
-To build an object of type :token:`ident`, one should provide the constructor
+To build an object of type :token:`ident`, provide the constructor
 :n:`@ident__0` with the appropriate number of terms filling the fields of the record.
 
 .. example::
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index 2904250e41..645986be9c 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -29,6 +29,7 @@ Private (matching) inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. attr:: private(matching)
+   :name: private(matching); Private
 
    This attribute can be used to forbid the use of the :g:`match`
    construct on objects of this inductive type outside of the module
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).
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 19c7c659e0..abecee8459 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -8,35 +8,36 @@ Proof schemes
 Generation of induction principles with ``Scheme``
 --------------------------------------------------------
 
-The ``Scheme`` command is a high-level tool for generating automatically
-(possibly mutual) induction principles for given types and sorts. Its
-syntax follows the schema:
+.. cmd:: Scheme {? @ident := } @scheme_kind {* with {? @ident := } @scheme_kind }
 
-.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort @sort {* with @ident__i := Induction for @ident__j Sort @sort}
+   .. insertprodn scheme_kind sort_family
 
-  This command is a high-level tool for generating automatically
+   .. prodn::
+      scheme_kind ::= Equality for @reference
+      | {| Induction | Minimality | Elimination | Case } for @reference Sort @sort_family
+      sort_family ::= Set
+      | Prop
+      | SProp
+      | Type
+
+  A high-level tool for automatically generating
   (possibly mutual) induction principles for given types and sorts.
-  Each :n:`@ident__j` is a different inductive type identifier belonging to
+  Each :n:`@reference` is a different inductive type identifier belonging to
   the same package of mutual inductive definitions.
-  The command generates the :n:`@ident__i`\s to be mutually recursive
-  definitions. Each term :n:`@ident__i` proves a general principle of mutual
-  induction for objects in type :n:`@ident__j`.
-
-.. cmdv:: Scheme @ident := Minimality for @ident Sort @sort {* with @ident := Minimality for @ident' Sort @sort}
-
-   Same as before but defines a non-dependent elimination principle more
-   natural in case of inductively defined relations.
+  The command generates the :n:`@ident`\s as mutually recursive
+  definitions. Each term :n:`@ident` proves a general principle of mutual
+  induction for objects in type :n:`@reference`.
 
-.. cmdv:: Scheme Equality for @ident
-   :name: Scheme Equality
+  :n:`@ident`
+    The name of the scheme. If not provided, the scheme name will be determined automatically
+    from the sorts involved.
 
-   Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident`
-   involves some other inductive types, their equality has to be defined first.
+  :n:`Minimality for @reference Sort @sort_family`
+    Defines a non-dependent elimination principle more natural for inductively defined relations.
 
-.. cmdv:: Scheme Induction for @ident Sort @sort {* with Induction for @ident Sort @sort}
-
-   If you do not provide the name of the schemes, they will be automatically computed from the
-   sorts involved (works also with Minimality).
+  :n:`Equality for @reference`
+     Tries to generate a Boolean equality and a proof of the decidability of the usual equality.
+     If :token:`reference` involves other inductive types, their equality has to be defined first.
 
 .. example::
 
@@ -138,13 +139,13 @@ Automatic declaration of schemes
 Combined Scheme
 ~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Combined Scheme @ident from {+, @ident__i}
+.. cmd:: Combined Scheme @ident__def from {+, @ident }
 
    This command is a tool for combining induction principles generated
    by the :cmd:`Scheme` command.
-   Each :n:`@ident__i` is a different inductive principle that must  belong
+   Each :n:`@ident` is a different inductive principle that must  belong
    to the same package of mutual inductive principle definitions.
-   This command generates :n:`@ident` to be the conjunction of the
+   This command generates :n:`@ident__def` as the conjunction of the
    principles: it is built from the common premises of the principles
    and concluded by the conjunction of their conclusions.
    In the case where all the inductive principles used are in sort
@@ -197,32 +198,30 @@ Combined Scheme
 Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
 
-.. cmd:: Derive Inversion @ident with @ident Sort @sort
-         Derive Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort
+.. cmd:: Derive Inversion @ident with @one_term {? Sort @sort_family }
 
-   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 :n:`{* @binder }` 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 {* @binder }, @ident @term`.
-   When applied, it is equivalent to having inverted the instance with the
-   tactic :g:`inversion`.
+   Generates an inversion lemma for the
+   :tacn:`inversion ... using ...` tactic.  :token:`ident` is the name
+   of the generated lemma.  :token:`one_term` should be in the form
+   :token:`qualid` or :n:`(forall {+ @binder }, @qualid @term)` where
+   :token:`qualid` is the name of an inductive
+   predicate and :n:`{+ @binder }` binds the variables occurring in the term
+   :token:`term`. The lemma is generated for the sort
+   :token:`sort_family` corresponding to :token:`one_term`.
+   Applying the lemma is equivalent to inverting the instance with the
+   :tacn:`inversion` tactic.
 
-.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort
-          Derive Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort
+.. cmd:: Derive Inversion_clear @ident with @one_term {? Sort @sort_family }
 
    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 {* @binder }, @ident @term) Sort @sort
+.. cmd:: Derive Dependent Inversion @ident with @one_term Sort @sort_family
 
    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 {* @binder }, @ident @term) Sort @sort
+.. cmd:: Derive Dependent Inversion_clear @ident with @one_term Sort @sort_family
 
    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 1791c53aa8..0c51361b64 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -385,8 +385,8 @@ a :token:`decl_notations` clause after the definition of the (co)inductive type
 (co)recursive term (or after the definition of each of them in case of mutual
 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. Note that only syntax modifiers that do not require to add or
-change a parsing rule are accepted.
+for records. Note that only syntax modifiers that do not require adding or
+changing a parsing rule are accepted.
 
    .. insertprodn decl_notations decl_notation
 
@@ -1894,12 +1894,12 @@ Tactic notations allow customizing the syntax of tactics.
         - :tacn:`unfold`, :tacn:`with_strategy`
 
       * - ``constr``
-        - :token:`term`
+        - :token:`one_term`
         - a term
         - :tacn:`exact`
 
       * - ``uconstr``
-        - :token:`term`
+        - :token:`one_term`
         - an untyped term
         - :tacn:`refine`
 
diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 738d64bfc3..93571ecebb 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -169,13 +169,24 @@ terminating functions.
 Tactics
 -------
 
-.. tacn:: functional induction (@qualid {+ @term})
+.. tacn:: functional induction @term {? using @one_term {? with @bindings } } {? as @simple_intropattern }
    :name: functional induction
 
-   The tactic functional induction performs case analysis and induction
-   following the definition of a function. It makes use of a principle
+   Performs case analysis and induction following the definition of a function
+   :token:`qualid`, which must be fully applied to its arguments as part of
+   :token:`term`. It uses a principle
    generated by :cmd:`Function` or :cmd:`Functional Scheme`.
    Note that this tactic is only available after a ``Require Import FunInd``.
+   See the :cmd:`Function` command.
+
+   :n:`using @one_term`
+     Specifies the induction principle (aka elimination scheme).
+
+   :n:`with @bindings`
+     Specifies the arguments of the induction principle.
+
+   :n:`as @simple_intropattern`
+     Provides names for the introduced variables.
 
    .. example::
 
@@ -189,15 +200,6 @@ Tactics
          Qed.
 
    .. note::
-      :n:`(@qualid {+ @term})` must be a correct full application
-      of :n:`@qualid`. In particular, the rules for implicit arguments are the
-      same as usual. For example use :n:`@@qualid` if you want to write implicit
-      arguments explicitly.
-
-   .. note::
-      Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
-
-   .. note::
       :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
       :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning
       phase, where :n:`@qualid` is the induction principle registered for :g:`f`
@@ -218,22 +220,27 @@ Tactics
    .. exn:: Not the right number of induction arguments.
       :undocumented:
 
-   .. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
-
-      Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving
-      explicitly the name of the introduced variables, the induction principle, and
-      the values of dependent premises of the elimination scheme, including
-      *predicates* for mutual induction when :n:`@qualid` is part of a mutually
-      recursive definition.
-
-.. tacn:: functional inversion @ident
+.. tacn:: functional inversion {| @ident | @natural } {? @qualid }
    :name: functional inversion
 
-   :tacn:`functional inversion` is a tactic that performs inversion on hypothesis
-   :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
-   {+ @term}` where :n:`@qualid` must have been defined using :cmd:`Function`.
+   Performs inversion on hypothesis
+   :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or
+   :n:`@term = @qualid {+ @term}` when :n:`@qualid` is defined using :cmd:`Function`.
    Note that this tactic is only available after a ``Require Import FunInd``.
 
+   :n:`@natural`
+     Does the same thing as :n:`intros until @natural` followed by
+     :n:`functional inversion @ident` where :token:`ident` is the
+     identifier for the last introduced hypothesis.
+
+   :n:`@qualid`
+     If the hypothesis :token:`ident` (or :token:`natural`) has a type of the form
+     :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
+     :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
+     functional inversion, this variant allows choosing which :token:`qualid`
+     is inverted.
+
+
    .. exn:: Hypothesis @ident must contain at least one Function.
       :undocumented:
 
@@ -242,39 +249,26 @@ Tactics
       This error may be raised when some inversion lemma failed to be generated by
       Function.
 
-
-   .. tacv:: functional inversion @natural
-
-      This does the same thing as :n:`intros until @natural` followed by
-      :n:`functional inversion @ident` where :token:`ident` is the
-      identifier for the last introduced hypothesis.
-
-   .. tacv:: functional inversion @ident @qualid
-             functional inversion @natural @qualid
-
-      If the hypothesis :token:`ident` (or :token:`natural`) has a type of the form
-      :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
-      :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
-      functional inversion, this variant allows choosing which :token:`qualid`
-      is inverted.
-
 .. _functional-scheme:
 
 Generation of induction principles with ``Functional`` ``Scheme``
 -----------------------------------------------------------------
 
 
-.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort}
+.. cmd:: Functional Scheme @func_scheme_def {* with @func_scheme_def }
+
+   .. insertprodn func_scheme_def func_scheme_def
+
+   .. prodn::
+      func_scheme_def ::= @ident := Induction for @qualid Sort @sort_family
+
+   An experimental high-level tool that
+   automatically generates induction principles corresponding to functions that
+   may be mutually recursive.  The command generates an
+   induction principle named :n:`@ident` for each given function named :n:`@qualid`.
+   The :n:`@qualid`\s must be given in the same order as when they were defined.
 
-   This command is a high-level experimental tool for
-   generating automatically induction principles corresponding to
-   (possibly mutually recursive) functions. First, it must be made
-   available via ``Require Import FunInd``.
-   Each :n:`@ident__i` is a different mutually defined function
-   name (the names must be in the same order as when they were defined). This
-   command generates the induction principle for each :n:`@ident__i`, following
-   the recursive structure and case analyses of the corresponding function
-   :n:`@ident__i'`.
+   Note the command must be made available via :cmd:`Require Import` ``FunInd``.
 
 .. warning::