Convert misc chapters to prodn

10 files changed, 446 insertions, 451 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.