Merge PR #9036: Add bodies to sphinx objects.

16 files changed, 893 insertions, 794 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 3d58f522dd..f523a39477 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -99,12 +99,12 @@ Extraction Options
 Setting the target language
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The ability to fix target language is the first and more important
-of the extraction options. Default is ``OCaml``.
+.. cmd:: Extraction Language ( OCaml | Haskell | Scheme )
+   :name: Extraction Language
+
+   The ability to fix target language is the first and more important
+   of the extraction options. Default is ``OCaml``.
 
-.. cmd:: Extraction Language OCaml
-.. cmd:: Extraction Language Haskell
-.. cmd:: Extraction Language Scheme
 
 Inlining and optimizations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -283,6 +283,7 @@ 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 => @string
+   :undocumented:
 
 The number of type variables is checked by the system. For example:
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 403b163196..e468cc63cd 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -530,19 +530,11 @@ Notice, however, that using the prefixed tactics it is possible to
 pass additional arguments such as ``using relation``.
 
 .. tacv:: setoid_reflexivity
-   :name: setoid_reflexivity
-
-.. tacv:: setoid_symmetry {? in @ident}
-   :name: setoid_symmetry
-
-.. tacv:: setoid_transitivity
-   :name: setoid_transitivity
-
-.. tacv:: setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident}
-   :name: setoid_rewrite
-
-.. tacv:: setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic}
-   :name: setoid_replace
+          setoid_symmetry {? in @ident}
+          setoid_transitivity
+          setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident}
+          setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic}
+   :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
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index fc5a366caf..c8fb4bd00e 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -128,13 +128,28 @@ Declaring Coercions
   the two given classes.
 
   .. exn:: @qualid not declared.
+     :undocumented:
+
   .. exn:: @qualid is already a coercion.
+     :undocumented:
+
   .. exn:: Funclass cannot be a source class.
+     :undocumented:
+
   .. exn:: @qualid is not a function.
+     :undocumented:
+
   .. exn:: Cannot find the source class of @qualid.
+     :undocumented:
+
   .. exn:: Cannot recognize @class as a source class of @qualid.
+     :undocumented:
+
   .. exn:: @qualid does not respect the uniform inheritance condition.
+     :undocumented:
+
   .. exn:: Found target class ... instead of ...
+     :undocumented:
 
   .. warn:: Ambiguous path.
 
@@ -202,34 +217,34 @@ declaration, this constructor is declared as a coercion.
 
 .. cmd:: Identity Coercion @ident : @class >-> @class
 
-  If ``C`` is the source `class` and ``D`` the destination, we check
-  that ``C`` is a constant with a body of the form
-  :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the
-  number of parameters of ``D``.  Then we define an identity
-  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``.
-
-  .. exn:: @class must be a transparent constant.
+   If ``C`` is the source `class` and ``D`` the destination, we check
+   that ``C`` is a constant with a body of the form
+   :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the
+   number of parameters of ``D``.  Then we define an identity
+   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``.
 
-  .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident
+   .. exn:: @class must be a transparent constant.
+      :undocumented:
 
-    Same as ``Identity Coercion`` but locally to the current section.
+   .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident
 
-  .. cmdv:: SubClass @ident := @type
-     :name: SubClass
+      Same as :cmd:`Identity Coercion` but locally to the current section.
 
-    If `type` is a class `ident'` applied to some arguments then
-    `ident` is defined and an identity coercion of name
-    `Id_ident_ident'` is
-    declared. Otherwise said, this is an abbreviation for
+   .. cmdv:: SubClass @ident := @type
+      :name: SubClass
 
-      ``Definition`` `ident` ``:=`` `type`.
+      If :n:`@type` is a class :n:`@ident'` applied to some arguments then
+      :n:`@ident` is defined and an identity coercion of name
+      :n:`Id_@ident_@ident'` is
+      declared. Otherwise said, this is an abbreviation for
 
-      ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`.
+      :n:`Definition @ident := @type.`
+      :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`.
 
-  .. cmdv:: Local SubClass @ident := @type
+   .. cmdv:: Local SubClass @ident := @type
 
-    Same as before but locally to the current section.
+      Same as before but locally to the current section.
 
 
 Displaying Available Coercions
@@ -237,19 +252,19 @@ Displaying Available Coercions
 
 .. cmd:: Print Classes
 
-  Print the list of declared classes in the current context.
+   Print the list of declared classes in the current context.
 
 .. cmd:: Print Coercions
 
-  Print the list of declared coercions in the current context.
+   Print the list of declared coercions in the current context.
 
 .. cmd:: Print Graph
 
-  Print the list of valid coercion paths in the current context.
+   Print the list of valid coercion paths in the current context.
 
 .. cmd:: Print Coercion Paths @class @class
 
-  Print the list of valid coercion paths between the two given classes.
+   Print the list of valid coercion paths between the two given classes.
 
 Activating the Printing of Coercions
 -------------------------------------
@@ -322,9 +337,9 @@ Coercions and Modules
 
 .. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it.
 
-          This warning is emitted when typechecking relies on a coercion
-          contained in a module that has not been explicitely imported. It helps
-          migrating code and stop relying on the option above.
+   This warning is emitted when typechecking relies on a coercion
+   contained in a module that has not been explicitely imported. It helps
+   migrating code and stop relying on the option above.
 
 Examples
 --------
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 2cde65dcdc..db8c09d88f 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -12,22 +12,22 @@ 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 SuchThat @term As @ident
-
-The first `ident` can appear in `term`. This command opens a new proof
-presenting the user with a goal for term in which the name `ident` is
-bound to an existential variable `?x` (formally, there are other goals
-standing for the existential variables but they are shelved, as
-described in :tacn:`shelve`).
-
-When the proof ends two constants are defined:
-
-+ The first one is named using the first `ident` and is defined as the proof of the
-  shelved goal (which is also the value of `?x`). It is always
-  transparent.
-+ The second one is named using the second `ident`. It has type `term`, and its body is
-  the proof of the initially visible goal. It is opaque if the proof
-  ends with ``Qed``, and transparent if the proof ends with ``Defined``.
+.. cmd:: Derive @ident__1 SuchThat @type 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
+   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`).
+
+   When the proof ends two constants are defined:
+
+   + The first one is named :n:`@ident__1` and is defined as the proof of the
+     shelved goal (which is also the value of :g:`?x`). It is always
+     transparent.
+   + The second one is named :n:`@ident__2`. It has type :n:`@type`, and its body is
+     the proof of the initially visible goal. It is opaque if the proof
+     ends with :cmd:`Qed`, and transparent if the proof ends with :cmd:`Defined`.
 
 .. example::
 
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 03d4f148e3..b008508bbc 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -67,16 +67,22 @@ is generated:
   :tacn:`intro` as many times as needed.
 
 .. exn:: omega: Unrecognized predicate or connective: @ident.
+   :undocumented:
 
 .. exn:: omega: Unrecognized atomic proposition: ...
+   :undocumented:
 
 .. exn:: omega: Can't solve a goal with proposition variables.
+   :undocumented:
 
 .. exn:: omega: Unrecognized proposition.
+   :undocumented:
 
 .. exn:: omega: Can't solve a goal with non-linear products.
+   :undocumented:
 
 .. exn:: omega: Can't solve a goal with equality on type ...
+   :undocumented:
 
 
 Using ``omega``
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index fad45995d2..cc8870e2e4 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -150,6 +150,7 @@ Program Definition
 
    .. exn:: @ident already exists.
       :name: @ident already exists. (Program Definition)
+      :undocumented:
 
    .. cmdv:: Program Definition @ident : @type := @term
 
@@ -162,7 +163,7 @@ Program Definition
       and the aforementioned coercion derivation are solved.
 
       .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
-
+         :undocumented:
 
    .. cmdv:: Program Definition @ident @binders : @type := @term
 
@@ -181,21 +182,21 @@ Program Fixpoint
 
 .. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term
 
-The optional order annotation follows the grammar:
+   The optional order annotation follows the grammar:
 
-.. productionlist:: orderannot
-   order      : measure `term` (`term`)? | wf `term` `term`
+   .. productionlist:: orderannot
+      order      : measure `term` (`term`)? | wf `term` `term`
 
-+ :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on
-  any subset of the arguments and the optional (parenthesised) term
-  ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R``
-  to ``lt``.
+   + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on
+     any subset of the arguments and the optional (parenthesised) term
+     ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R``
+     to ``lt``.
 
-+ :g:`wf R x` which is equivalent to :g:`measure x (R)`.
+   + :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.
+   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.
 
 .. coqtop:: reset in
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 58617916c0..5bab63f6d0 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -100,26 +100,26 @@ Concrete usage in Coq
 
 .. tacn:: ring
 
-The ``ring`` tactic solves equations upon polynomial expressions of a ring
-(or semiring) structure. It proceeds by normalizing both sides
-of the equation (w.r.t. associativity, commutativity and
-distributivity, constant propagation, rewriting of monomials) and
-comparing syntactically the results.
+   This tactic solves equations upon polynomial expressions of a ring
+   (or semiring) structure. It proceeds by normalizing both sides
+   of the equation (w.r.t. associativity, commutativity and
+   distributivity, constant propagation, rewriting of monomials) and
+   comparing syntactically the results.
 
 .. tacn:: ring_simplify
 
-``ring_simplify`` 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
-is given, then the conclusion should be an equation and both
-sides are normalized. The tactic can also be applied in a hypothesis.
+   This tactic 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
+   is given, then the conclusion should be an equation and both
+   sides are normalized. The tactic can also be applied in a hypothesis.
 
-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
-first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do
-``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do
-``Require Import NArithRing`` or ``Require Import NArith``.
+   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
+   first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do
+   ``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do
+   ``Require Import NArithRing`` or ``Require Import NArith``.
 
 
 .. example::
@@ -141,25 +141,24 @@ first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do
 
 .. tacv:: ring [{* @term }] 
  
-decides the equality of two terms modulo ring operations and 
-the equalities defined by the :n:`@term`\ s.
-Each :n:`@term` has to be a proof of some equality `m = p`, where `m` is a monomial (after “abstraction”), `p` a polynomial and `=` the corresponding equality of the ring structure.
+   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
  
-performs the simplification in the hypothesis named :n:`@ident`.
+   This tactic performs the simplification in the hypothesis named :token:`ident`.
 
 
 .. note:: 
 
-  .. tacn::  ring_simplify @term1; ring_simplify @term2 
+  :n:`ring_simplify @term__1; ring_simplify @term__2` is not equivalent to
+  :n:`ring_simplify @term__1 @term__2`.
 
-  is not equivalent to 
-
-  .. tacn:: ring_simplify @term1 @term2
-
-  In the latter case the variables map
-  is shared between the two terms, and common subterm `t` of :n:`@term1` and :n:`@term2`
+  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.
@@ -174,17 +173,17 @@ Error messages:
 
 .. exn:: Arguments of ring_simplify do not have all the same type.
   
-  ``ring_simplify`` cannot simplify terms of several rings at the same
+  :tacn:`ring_simplify` cannot simplify terms of several rings at the same
   time. Invoke the tactic once per ring structure.
 
 .. exn:: Cannot find a declared ring structure over @term.
 
   No ring has been declared for the type of the terms to be simplified.
-  Use ``Add Ring`` first.
+  Use :cmd:`Add Ring` first.
 
 .. exn:: Cannot find a declared ring structure for equality @term.
 
-  Same as above in the case of the ``ring`` tactic.
+  Same as above in the case of the :tacn:`ring` tactic.
 
 
 Adding a ring structure
@@ -302,93 +301,93 @@ The syntax for adding a new ring is
 
 .. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}
 
-The :n:`@ident` is not relevant. It is used just for error messages. The
-:n:`@term` is a proof that the ring signature satisfies the (semi-)ring
-axioms. The optional list of modifiers is used to tailor the behavior
-of the tactic. The following list describes their syntax and effects:
-
-.. productionlist:: coq
-   ring_mod : abstract | decidable `term` | morphism `term`
-            : | setoid `term` `term`
-            : | constants [`ltac`]
-            : | preprocess [`ltac`]
-            : | postprocess [`ltac`]
-            : | power_tac `term` [`ltac`]
-            : | sign `term`
-            : | div `term`
-
-abstract
-  declares the ring as abstract. This is the default.
-
-decidable :n:`@term`
-  declares the ring as computational. The expression
-  :n:`@term` is the correctness proof of an equality test ``?=!``
-  (which  hould be evaluable). Its type should be of the form 
-  ``forall x y, x ?=! y = true → x == y``.
-
-morphism :n:`@term`
-  declares the ring as a customized one. The expression
-  :n:`@term` is a proof that there exists a morphism between a set of
-  coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and
-  ``Ring_theory.semi_morph``).
-
-setoid :n:`@term` :n:`@term` 
-  forces the use of given setoid. The first
-  :n:`@term` is a proof that the equality is indeed a setoid (see
-  ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the
-  ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and 
-  ``Ring_theory.sring_eq_ext``).
-  This modifier needs not be used if the setoid and morphisms have been
-  declared.
-
-constants [:n:`@ltac`] 
-  specifies a tactic expression :n:`@ltac` that, given a
-  term, returns either an object of the coefficient set that is mapped
-  to the expression via the morphism, or returns
-  ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1
-  to their counterpart in the coefficient set. This is generally not
-  desirable for non trivial computational rings.
-
-preprocess [:n:`@ltac`]
-  specifies a tactic :n:`@ltac` that is applied as a
-  preliminary step for ``ring`` and ``ring_simplify``. It can be used to
-  transform a goal so that it is better recognized. For instance, ``S n``
-  can be changed to ``plus 1 n``.
-
-postprocess [:n:`@ltac`]
-  specifies a tactic :n:`@ltac` that is applied as a final
-  step for ``ring_simplify``. For instance, it can be used to undo
-  modifications of the preprocessor.
-
-power_tac :n:`@term` [:n:`@ltac`] 
-  allows ``ring`` and ``ring_simplify`` to recognize
-  power expressions with a constant positive integer exponent (example:
-  ::math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies
-  the specification of a power function (term has to be a proof of
-  ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression
-  that, given a term, “abstracts” it into an object of type |N| whose
-  interpretation via ``Cp_phi`` (the evaluation function of power
-  coefficient) is the original term, or returns ``InitialRing.NotConstant``
-  if not a constant coefficient (i.e. |L_tac| is the inverse function of
-  ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v``
-  and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic
-  does not recognize power expressions as ring expressions.
-
-sign :n:`@term`
-  allows ``ring_simplify`` to use a minus operation when
-  outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
-  term `:n:`@term` is a proof that a given sign function indicates expressions
-  that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See
-  ``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
-
-div :n:`@term`
-  allows ``ring`` and ``ring_simplify`` to use monomials with
-  coefficients other than 1 in the rewriting. The term :n:`@term` is a proof
-  that a given division function satisfies the specification of an
-  euclidean division function (:n:`@term` has to be a proof of
-  ``Ring_theory.div_theory``). For example, this function is called when
-  trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See
-  ``plugins/setoid_ring/InitialRing.v`` for examples of div function.
+   The :token:`ident` is not relevant. It is used just for error messages. The
+   :token:`term` is a proof that the ring signature satisfies the (semi-)ring
+   axioms. The optional list of modifiers is used to tailor the behavior
+   of the tactic. The following list describes their syntax and effects:
+
+   .. productionlist:: coq
+      ring_mod : abstract | decidable `term` | morphism `term`
+               : | setoid `term` `term`
+               : | constants [`ltac`]
+               : | preprocess [`ltac`]
+               : | postprocess [`ltac`]
+               : | power_tac `term` [`ltac`]
+               : | sign `term`
+               : | div `term`
+
+   abstract
+      declares the ring as abstract. This is the default.
+
+   decidable :n:`@term`
+      declares the ring as computational. The expression
+      :n:`@term` is the correctness proof of an equality test ``?=!``
+      (which  hould be evaluable). Its type should be of the form
+      ``forall x y, x ?=! y = true → x == y``.
+
+   morphism :n:`@term`
+      declares the ring as a customized one. The expression
+      :n:`@term` is a proof that there exists a morphism between a set of
+      coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and
+      ``Ring_theory.semi_morph``).
+
+   setoid :n:`@term` :n:`@term`
+      forces the use of given setoid. The first
+      :n:`@term` is a proof that the equality is indeed a setoid (see
+      ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the
+      ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and
+      ``Ring_theory.sring_eq_ext``).
+      This modifier needs not be used if the setoid and morphisms have been
+      declared.
+
+   constants [ :n:`@ltac` ]
+      specifies a tactic expression :n:`@ltac` that, given a
+      term, returns either an object of the coefficient set that is mapped
+      to the expression via the morphism, or returns
+      ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1
+      to their counterpart in the coefficient set. This is generally not
+      desirable for non trivial computational rings.
+
+   preprocess [ :n:`@ltac` ]
+      specifies a tactic :n:`@ltac` that is applied as a
+      preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to
+      transform a goal so that it is better recognized. For instance, ``S n``
+      can be changed to ``plus 1 n``.
+
+   postprocess [ :n:`@ltac` ]
+      specifies a tactic :n:`@ltac` that is applied as a final
+      step for :tacn:`ring_simplify`. For instance, it can be used to undo
+      modifications of the preprocessor.
+
+   power_tac :n:`@term` [ :n:`@ltac` ]
+      allows :tacn:`ring` and :tacn:`ring_simplify` to recognize
+      power expressions with a constant positive integer exponent (example:
+      :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies
+      the specification of a power function (term has to be a proof of
+      ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression
+      that, given a term, “abstracts” it into an object of type |N| whose
+      interpretation via ``Cp_phi`` (the evaluation function of power
+      coefficient) is the original term, or returns ``InitialRing.NotConstant``
+      if not a constant coefficient (i.e. |L_tac| is the inverse function of
+      ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v``
+      and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic
+      does not recognize power expressions as ring expressions.
+
+   sign :n:`@term`
+      allows :tacn:`ring_simplify` to use a minus operation when
+      outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
+      term `:n:`@term` is a proof that a given sign function indicates expressions
+      that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See
+      ``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
+
+   div :n:`@term`
+      allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with
+      coefficients other than 1 in the rewriting. The term :n:`@term` is a proof
+      that a given division function satisfies the specification of an
+      euclidean division function (:n:`@term` has to be a proof of
+      ``Ring_theory.div_theory``). For example, this function is called when
+      trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See
+      ``plugins/setoid_ring/InitialRing.v`` for examples of div function.
 
 Error messages:
 
@@ -497,30 +496,31 @@ Dealing with fields
 
 .. tacn:: field
 
-The ``field`` tactic is an extension of the ``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`.
-Note that ``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
-which is a conjunction if there are several denominators. Nonzero
-conditions are always polynomial expressions. For example when
-reducing the expression :math:`1/(1 + 1/x)`, two side conditions are
-generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since
-a field is an integral domain, and when the equality test on
-coefficients is complete w.r.t. the equality of the target field,
-constants can be proven different from zero automatically.
-
-The tactic must be loaded by ``Require Import Field``. New field
-structures can be declared to the system with the ``Add Field`` command
-(see below). The field of real numbers is defined in module ``RealField``
-(in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so
-that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on
-real numbers. Rational numbers in canonical form are also declared as
-a field in the module ``Qcanon``.
+   This tactic is 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`.
+
+   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
+   which is a conjunction if there are several denominators. Nonzero
+   conditions are always polynomial expressions. For example when
+   reducing the expression :math:`1/(1 + 1/x)`, two side conditions are
+   generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since
+   a field is an integral domain, and when the equality test on
+   coefficients is complete w.r.t. the equality of the target field,
+   constants can be proven different from zero automatically.
+
+   The tactic must be loaded by ``Require Import Field``. New field
+   structures can be declared to the system with the ``Add Field`` command
+   (see below). The field of real numbers is defined in module ``RealField``
+   (in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so
+   that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on
+   real numbers. Rational numbers in canonical form are also declared as
+   a field in the module ``Qcanon``.
 
 
 .. example::
@@ -654,27 +654,25 @@ The syntax for adding a new field is
 
 .. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}
 
-The :n:`@ident` is not relevant. It is used just for error
-messages. :n:`@term` is a proof that the field signature satisfies the
-(semi-)field axioms. The optional list of modifiers is used to tailor
-the behavior of the tactic.
-
-.. productionlist:: coq
-   field_mod : `ring_mod` | completeness `term`
-
-Since field tactics are built upon ``ring``
-tactics, all modifiers of the ``Add Ring`` apply. There is only one
-specific modifier:
-
-completeness :n:`@term`
-  allows the field tactic to prove automatically
-  that the image of nonzero coefficients are mapped to nonzero
-  elements of the field. :n:`@term` is a proof of
-
-  ``forall x y, [x] == [y] ->  x ?=! y = true``, 
-
-  which is the completeness of equality on coefficients
-  w.r.t. the field equality.
+   The :n:`@ident` is not relevant. It is used just for error
+   messages. :n:`@term` is a proof that the field signature satisfies the
+   (semi-)field axioms. The optional list of modifiers is used to tailor
+   the behavior of the tactic.
+
+   .. productionlist:: coq
+      field_mod : `ring_mod` | completeness `term`
+
+   Since field tactics are built upon ``ring``
+   tactics, all modifiers of the ``Add Ring`` apply. There is only one
+   specific modifier:
+
+   completeness :n:`@term`
+      allows the field tactic to prove automatically
+      that the image of nonzero coefficients are mapped to nonzero
+      elements of the field. :n:`@term` is a proof of
+      :g:`forall x y, [x] == [y] ->  x ?=! y = true`,
+      which is the completeness of equality on coefficients
+      w.r.t. the field equality.
 
 
 History of ring
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 369dae0ead..15a55d9e72 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -298,24 +298,24 @@ Variants:
 
       This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
+.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
 
-The :cmd:`Instance` command is used to declare a typeclass instance named
-``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and
-fields ``b1`` to ``bi``, where each field must be a declared field of
-the class.  Missing fields must be filled in interactive proof mode.
+   This command is used to declare a typeclass instance named
+   :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and
+   fields ``b1`` to ``bi``, where each field must be a declared field of
+   the class.  Missing fields must be filled in interactive proof mode.
 
-An arbitrary context of ``binders`` 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 is not specified, it defaults to the number
-of non-dependent binders of the instance.
+   An arbitrary context of :token:`binders` 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 is not specified, it defaults to the number
+   of non-dependent binders of the instance.
 
-.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term
+.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term
 
    This syntax is used for declaration of singleton class instances or
-   for directly giving an explicit term of type ``forall binders, Class
-   t1 … tn``.  One need not even mention the unique field name for
+   for directly giving an explicit term of type :n:`forall @binders, @class
+   @term__1 … @term__n`.  One need not even mention the unique field name for
    singleton classes.
 
 .. cmdv:: Global Instance
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 41afe3c312..99b883d23c 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -386,8 +386,10 @@ to universes and explicitly instantiate polymorphic definitions.
    global constraint on polymorphic universes.
 
    .. exn:: Undeclared universe @ident.
+      :undocumented:
 
    .. exn:: Universe inconsistency.
+      :undocumented:
 
 
 Polymorphic definitions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 391afcb1f7..562ed48171 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -27,22 +27,20 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
      field          : `ident` [ `binders` ] : `type` [ where `notation` ]
                     : | `ident` [ `binders` ] [: `type` ] := `term`
 
-In the expression:
-
 .. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } }
 
-the first identifier :token:`ident` is the name of the defined record and :token:`sort` is its
-type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted,
-the default name ``Build_``\ :token:`ident`, where :token:`ident` is the record name, is used. If :token:`sort` is
-omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of
-fields. For a given field :token:`ident`, its type is :g:`forall binders, type`.
-Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the
-order of the fields is important. Finally, :token:`binders` are parameters of the record.
+   The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its
+   type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted,
+   the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is
+   omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of
+   fields. For a given field :token:`ident`, its type is :n:`forall @binders, @type`.
+   Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the
+   order of the fields is important. Finally, :token:`binders` are parameters of the record.
 
 More generally, a record may have explicitly defined (a.k.a. manifest)
 fields. For instance, we might have:
-:n:`Record @ident @binders : @sort := { @ident₁ : @type₁ ; @ident₂ := @term₂ ; @ident₃ : @type₃ }`.
-in which case the correctness of :n:`@type₃` may rely on the instance :n:`@term₂` of :n:`@ident₂` and :n:`@term₂` may in turn depend on :n:`@ident₁`.
+:n:`Record @ident @binders : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`.
+in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`.
 
 .. example::
 
@@ -149,16 +147,16 @@ available:
 
    Eval compute in half.(top).
 
-It can be activated for printing with
-
 .. flag:: Printing Projections
 
-.. example::
+   This flag activates the dot notation for printing.
 
-    .. coqtop:: all
+   .. example::
+
+      .. coqtop:: all
 
-       Set Printing Projections.
-       Check top half.
+         Set Printing Projections.
+         Check top half.
 
 .. FIXME: move this to the main grammar in the spec chapter
 
@@ -601,17 +599,17 @@ The following experimental command is available when the ``FunInd`` library has
 
 .. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term
 
-This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
-for several ways of defining a function *and other useful related
-objects*, namely: an induction principle that reflects the recursive
-structure of the function (see :tacn:`function induction`) and its fixpoint equality.
-The meaning of this declaration is to define a function ident,
-similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must
-be given (unless the function is not recursive), but it might not
-necessarily be *structurally* decreasing. The point of the {} annotation
-is to name the decreasing argument *and* to describe which kind of
-decreasing criteria must be used to ensure termination of recursive
-calls.
+   This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
+   for several ways of defining a function *and other useful related
+   objects*, namely: an induction principle that reflects the recursive
+   structure of the function (see :tacn:`function induction`) and its fixpoint equality.
+   The meaning of this declaration is to define a function ident,
+   similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must
+   be given (unless the function is not recursive), but it might not
+   necessarily be *structurally* decreasing. The point of the {} annotation
+   is to name the decreasing argument *and* to describe which kind of
+   decreasing criteria must be used to ensure termination of recursive
+   calls.
 
 The ``Function`` construction also enjoys the ``with`` extension to define
 mutually recursive definitions. However, this feature does not work
@@ -667,27 +665,32 @@ For now, dependent cases are not treated for non structurally
 terminating functions.
 
 .. exn:: The recursive argument must be specified.
+   :undocumented:
+
 .. exn:: No argument name @ident.
+   :undocumented:
+
 .. exn:: Cannot use mutual definition with well-founded recursion or measure.
+   :undocumented:
 
 .. warn:: Cannot define graph for @ident.
 
-    The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident
-    raised a typing error. Only `ident` is defined; the induction scheme
-    will not be generated. This error happens generally when:
+   The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident
+   raised a typing error. Only :token:`ident` is defined; the induction scheme
+   will not be generated. This error happens generally when:
 
-    - the definition uses pattern matching on dependent types,
-      which ``Function`` cannot deal with yet.
-    - the definition is not a *pattern matching tree* as explained above.
+   - the definition uses pattern matching on dependent types,
+     which ``Function`` cannot deal with yet.
+   - the definition is not a *pattern matching tree* as explained above.
 
 .. warn:: Cannot define principle(s) for @ident.
 
-     The generation of the graph relation (`R_ident`) succeeded but the induction principle
-     could not be built. Only `ident` is defined. Please report.
+   The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle
+   could not be built. Only :token:`ident` is defined. Please report.
 
 .. warn:: Cannot build functional inversion principle.
 
-     `functional inversion` will not be available for the function.
+   :tacn:`functional inversion` will not be available for the function.
 
 .. seealso:: :ref:`functional-scheme` and :tacn:`function induction`
 
@@ -713,7 +716,7 @@ used by ``Function``. A more precise description is given below.
     + The fixpoint equation of `ident`: `ident_equation`.
 
 .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term
-.. cmdv:: Function @ident {* @binder } { wf @term @ident } : @type := @term
+          Function @ident {* @binder } { wf @term @ident } : @type := @term
 
    Defines a recursive function by well-founded recursion. The module ``Recdef``
    of the standard library must be loaded for this feature. The ``{}``
@@ -799,10 +802,10 @@ Section :ref:`gallina-definitions`).
     `s1` and outside.
 
     .. exn:: This is not the last opened section.
+       :undocumented:
 
-**Remarks:**
-
-#. Most commands, like ``Hint``, ``Notation``, option management, … which
+.. note::
+   Most commands, like ``Hint``, ``Notation``, option management, … which
    appear inside a section are canceled when the section is closed.
 
 
@@ -874,52 +877,55 @@ Reserved commands inside an interactive module
 
 .. cmd:: Include {+<+ @module}
 
-   is a shortcut for the commands ``Include`` `module` for each `module`.
+   is a shortcut for the commands :n:`Include @module` for each :token:`module`.
 
 .. cmd:: End @ident
 
-   This command closes the interactive module `ident`. If the module type
+   This command closes the interactive module :token:`ident`. If the module type
    was given the content of the module is matched against it and an error
    is signaled if the matching fails. If the module is basic (is not a
    functor) its components (constants, inductive types, submodules etc.)
    are now available through the dot notation.
 
     .. exn:: No such label @ident.
+       :undocumented:
 
     .. exn:: Signature components for label @ident do not match.
+       :undocumented:
 
     .. exn:: This is not the last opened module.
+       :undocumented:
 
 .. cmd:: Module @ident := @module_expression
 
-    This command defines the module identifier `ident` to be equal
-    to `module_expression`.
+    This command defines the module identifier :token:`ident` to be equal
+    to :token:`module_expression`.
 
     .. cmdv:: Module @ident {* @module_binding} := @module_expression
 
-       Defines a functor with parameters given by the list of `module_binding` and body `module_expression`.
+       Defines a functor with parameters given by the list of :token:`module_binding` and body :token:`module_expression`.
 
     .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression
 
-       Defines a functor with parameters given by the list of `module_binding` (possibly none), and output module type `module_type`,
-       with body `module_expression`.
+       Defines a functor with parameters given by the list of :token:`module_binding` (possibly none), and output module type :token:`module_type`,
+       with body :token:`module_expression`.
 
     .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression
 
-       Defines a functor with parameters given by module_bindings (possibly none) with body `module_expression`.
+       Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`.
        The body is checked against each |module_type_i|.
 
     .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}
 
-       is equivalent to an interactive module where each `module_expression` is included.
+       is equivalent to an interactive module where each :token:`module_expression` is included.
 
 .. cmd:: Module Type @ident
 
-This command is used to start an interactive module type `ident`.
+   This command is used to start an interactive module type :token:`ident`.
 
-    .. cmdv:: Module Type @ident {* @module_binding}
+   .. cmdv:: Module Type @ident {* @module_binding}
 
-       Starts an interactive functor type with parameters given by `module_bindings`.
+      Starts an interactive functor type with parameters given by :token:`module_bindings`.
 
 
 Reserved commands inside an interactive module type:
@@ -931,7 +937,7 @@ Reserved commands inside an interactive module type:
 
 .. cmd:: Include {+<+ @module}
 
-   is a shortcut for the command ``Include`` `module` for each `module`.
+   This is a shortcut for the command :n:`Include @module` for each :token:`module`.
 
 .. cmd:: @assumption_keyword Inline @assums
    :name: Inline
@@ -941,31 +947,32 @@ Reserved commands inside an interactive module type:
 
 .. cmd:: End @ident
 
-   This command closes the interactive module type `ident`.
+   This command closes the interactive module type :token:`ident`.
 
    .. exn:: This is not the last opened module type.
+      :undocumented:
 
 .. cmd:: Module Type @ident := @module_type
 
-   Defines a module type `ident` equal to `module_type`.
+   Defines a module type :token:`ident` equal to :token:`module_type`.
 
     .. cmdv:: Module Type @ident {* @module_binding} := @module_type
 
-       Defines a functor type `ident` specifying functors taking arguments `module_bindings` and
-       returning `module_type`.
+       Defines a functor type :token:`ident` specifying functors taking arguments :token:`module_bindings` and
+       returning :token:`module_type`.
 
     .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type }
 
-       is equivalent to an interactive module type were each `module_type` is included.
+       is equivalent to an interactive module type were each :token:`module_type` is included.
 
 .. cmd:: Declare Module @ident : @module_type
 
-   Declares a module `ident` of type `module_type`.
+   Declares a module :token:`ident` of type :token:`module_type`.
 
     .. cmdv:: Declare Module @ident {* @module_binding} : @module_type
 
-       Declares a functor with parameters given by the list of `module_binding` and output module type
-       `module_type`.
+       Declares a functor with parameters given by the list of :token:`module_binding` and output module type
+       :token:`module_type`.
 
 .. example::
 
@@ -1205,8 +1212,10 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
        is imported, qualid is imported as well.
 
     .. exn:: @qualid is not a module.
+       :undocumented:
 
     .. warn:: Trying to mask the absolute name @qualid!
+       :undocumented:
 
 .. cmd:: Print Module @ident
 
@@ -1506,6 +1515,7 @@ possible, the correct argument will be automatically generated.
 
 .. exn:: Cannot infer a term for this placeholder.
    :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments)
+   :undocumented:
 
    |Coq| was not able to deduce an instantiation of a “_”.
 
@@ -1566,38 +1576,39 @@ usual implicit arguments disambiguation syntax.
 Declaring Implicit Arguments
 ++++++++++++++++++++++++++++
 
-To set implicit arguments *a posteriori*, one can use the command:
 
-.. cmd:: Arguments @qualid {* @possibly_bracketed_ident }
-   :name: Arguments (implicits)
 
-where the list of `possibly_bracketed_ident` is a prefix of the list of
-arguments of `qualid` where the ones to be declared implicit are
-surrounded by square brackets and the ones to be declared as maximally
-inserted implicits are surrounded by curly braces.
+.. cmd:: Arguments @qualid {* [ @ident ] | @ident }
+   :name: Arguments (implicits)
 
-After the above declaration is issued, implicit arguments can just
-(and have to) be skipped in any expression involving an application
-of `qualid`.
+   This command is used to set implicit arguments *a posteriori*,
+   where the list of possibly bracketed :token:`ident` is a prefix of the list of
+   arguments of :token:`qualid` where the ones to be declared implicit are
+   surrounded by square brackets and the ones to be declared as maximally
+   inserted implicits are surrounded by curly braces.
 
-Implicit arguments can be cleared with the following syntax:
+   After the above declaration is issued, implicit arguments can just
+   (and have to) be skipped in any expression involving an application
+   of :token:`qualid`.
 
 .. cmd:: Arguments @qualid : clear implicits
 
-.. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident }
+   This command clears implicit arguments.
+
+.. cmdv:: Global Arguments @qualid {* [ @ident ] | @ident }
 
-   Says to recompute the implicit arguments of
-   `qualid` after ending of the current section if any, enforcing the
+   This command is used to recompute the implicit arguments of
+   :token:`qualid` after ending of the current section if any, enforcing the
    implicit arguments known from inside the section to be the ones
    declared by the command.
 
-.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident }
+.. cmdv:: Local Arguments @qualid {* [ @ident ] | @ident }
 
    When in a module, tell not to activate the
-   implicit arguments ofqualid declared by this command to contexts that
+   implicit arguments of :token:`qualid` declared by this command to contexts that
    require the module.
 
-.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } }
+.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | @ident } }
 
    For names of constants, inductive types,
    constructors, lemmas which can only be applied to a fixed number of
@@ -1639,33 +1650,34 @@ Implicit arguments can be cleared with the following syntax:
 
        Check (fun l => map length l = map (list nat) nat length l).
 
-Remark: To know which are the implicit arguments of an object, use the
-command ``Print Implicit`` (see :ref:`displaying-implicit-args`).
+.. note::
+   To know which are the implicit arguments of an object, use the
+   command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`).
 
 
 Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-|Coq| can also automatically detect what are the implicit arguments of a
-defined object. The command is just
-
 .. cmd:: Arguments @qualid : default implicits
 
-The auto-detection is governed by options telling if strict,
-contextual, or reversible-pattern implicit arguments must be
-considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`,
-:ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`).
+   This command tells |Coq| to automatically detect what are the implicit arguments of a
+   defined object.
+
+   The auto-detection is governed by options telling if strict,
+   contextual, or reversible-pattern implicit arguments must be
+   considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`,
+   :ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`).
 
-.. cmdv:: Global Arguments @qualid : default implicits
+   .. cmdv:: Global Arguments @qualid : default implicits
 
-    Tell to recompute the
-    implicit arguments of qualid after ending of the current section if
-    any.
+      Tell to recompute the
+      implicit arguments of qualid after ending of the current section if
+      any.
 
-.. cmdv:: Local Arguments @qualid : default implicits
+   .. cmdv:: Local Arguments @qualid : default implicits
 
-       When in a module, tell not to activate the implicit arguments of `qualid` computed by this
-       declaration to contexts that requires the module.
+      When in a module, tell not to activate the implicit arguments of :token:`qualid` computed by this
+      declaration to contexts that requires the module.
 
 .. example::
 
@@ -1820,10 +1832,10 @@ This syntax extension is given in the following grammar:
 Renaming implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Implicit arguments names can be redefined using the following syntax:
-
 .. cmd:: Arguments @qualid {* @name} : @rename
 
+   This command is used to redefine the names of implicit arguments.
+
 With the assert flag, ``Arguments`` can be used to assert that a given
 object has the expected number of arguments and that these arguments
 are named as expected.
@@ -1845,11 +1857,12 @@ are named as expected.
 Displaying what the implicit arguments are
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-To display the implicit arguments associated to an object, and to know
-if each of them is to be used maximally or not, use the command
-
 .. cmd:: Print Implicit @qualid
 
+   Use this command to display the implicit arguments associated to an object,
+   and to know if each of them is to be used maximally or not.
+
+
 Explicit displaying of implicit arguments for pretty-printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1984,16 +1997,16 @@ Implicit types of variables
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 It is possible to bind variable names to a given type (e.g. in a
-development using arithmetic, it may be convenient to bind the names `n`
-or `m` to the type ``nat`` of natural numbers). The command for that is
+development using arithmetic, it may be convenient to bind the names :g:`n`
+or :g:`m` to the type :g:`nat` of natural numbers).
 
 .. cmd:: Implicit Types {+ @ident } : @type
 
-The effect of the command is to automatically set the type of bound
-variables starting with `ident` (either `ident` itself or `ident` followed by
-one or more single quotes, underscore or digits) to be `type` (unless
-the bound variable is already declared with an explicit type in which
-case, this latter type is considered).
+   The effect of the command is to automatically set the type of bound
+   variables starting with :token:`ident` (either :token:`ident` itself or
+   :token:`ident` followed by one or more single quotes, underscore or
+   digits) to be :token:`type` (unless the bound variable is already declared
+   with an explicit type in which case, this latter type is considered).
 
 .. example::
 
@@ -2137,29 +2150,29 @@ Printing universes
    terms apparently identical but internally different in the Calculus of Inductive
    Constructions.
 
-The constraints on the internal level of the occurrences of Type
-(see :ref:`Sorts`) can be printed using the command
-
 .. cmd:: Print {? Sorted} Universes
    :name: Print Universes
 
-If the optional ``Sorted`` option is given, each universe will be made
-equivalent to a numbered label reflecting its level (with a linear
-ordering) in the universe hierarchy.
+   This command can be used to print the constraints on the internal level
+   of the occurrences of :math:`\Type` (see :ref:`Sorts`).
+
+   If the optional ``Sorted`` option is given, each universe will be made
+   equivalent to a numbered label reflecting its level (with a linear
+   ordering) in the universe hierarchy.
 
-This command also accepts an optional output filename:
+   .. cmdv:: Print {? Sorted} Universes @string
 
-.. cmdv:: Print {? Sorted} Universes @string
+      This variant accepts an optional output filename.
 
-If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
-language, and can be processed by Graphviz tools. The format is
-unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
+      If :token:`string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
+      language, and can be processed by Graphviz tools. The format is
+      unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
 .. cmdv:: Print Universes Subgraph(@names)
 
-Prints the graph restricted to the requested names (adjusting
-constraints to preserve the implied transitive constraints between
-kept universes).
+   Prints the graph restricted to the requested names (adjusting
+   constraints to preserve the implied transitive constraints between
+   kept universes).
 
 .. _existential-variables:
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index edd83b7cee..0ea8c7be2d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -292,6 +292,7 @@ focused goals with:
 
    .. exn:: No such goal.
       :name: No such goal. (Goal selector)
+      :undocumented:
 
    .. TODO change error message index entry
 
@@ -351,6 +352,7 @@ We can check if a tactic made progress with:
    goals (up to syntactical equality), then an error of level 0 is raised.
 
    .. exn:: Failed to progress.
+      :undocumented:
 
 Backtracking branching
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -393,6 +395,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
    :n:`v__i` to have *at least* one success.
 
    .. exn:: No applicable tactic.
+      :undocumented:
 
    .. tacv:: first @expr
 
@@ -482,6 +485,7 @@ one* success:
       immediately.
 
    .. exn:: This tactic has more than one success.
+      :undocumented:
 
 Checking the failure
 ~~~~~~~~~~~~~~~~~~~~
@@ -521,6 +525,7 @@ among a panel of tactics:
    apply :n:`v__2` and so on. It fails if there is no solving tactic.
 
    .. exn:: Cannot solve the goal.
+      :undocumented:
 
    .. tacv:: solve @expr
 
@@ -576,8 +581,7 @@ Failing
       goals left. See the example for clarification.
 
    .. tacv:: gfail {* message_token}
-
-   .. tacv:: gfail @num {* message_token}
+             gfail @num {* message_token}
 
       These variants fail with an error message or an error level even if
       there are no goals left. Be careful however if Coq terms have to be
@@ -586,9 +590,11 @@ Failing
       evaluated, a tactic call like :n:`let x := H in fail 0 x` will succeed.
 
    .. exn:: Tactic Failure message (level @num).
+      :undocumented:
 
    .. exn:: No such goal.
       :name: No such goal. (fail)
+      :undocumented:
 
    .. example::
 
@@ -670,24 +676,24 @@ tactic
 
    This tactic currently does not support nesting, and will report times
    based on the innermost execution. This is due to the fact that it is
-   implemented using the tactics
+   implemented using the following internal tactics:
 
    .. tacn:: restart_timer @string
       :name: restart_timer
 
-   and
+      Reset a timer
 
-   .. tacn:: finish_timing {? @string} @string
+   .. tacn:: finish_timing {? (@string)} @string
       :name: finish_timing
 
-   which (re)set and display an optionally named timer, respectively. The
-   parenthesized string argument to :n:`finish_timing` is also optional, and
-   determines the label associated with the timer for printing.
+      Display an optionally named timer. The parenthesized string argument
+      is also optional, and determines the label associated with the timer
+      for printing.
 
-   By copying the definition of :n:`time_constr` from the standard library,
+   By copying the definition of :tacn:`time_constr` from the standard library,
    users can achive support for a fixed pattern of nesting by passing
-   different :n:`@string` parameters to :n:`restart_timer` and :n:`finish_timing`
-   at each level of nesting.
+   different :token:`string` parameters to :tacn:`restart_timer` and
+   :tacn:`finish_timing` at each level of nesting.
 
    .. example::
 
@@ -967,10 +973,10 @@ Evaluation of a term can be performed with:
 Recovering the type of a term
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The following returns the type of term:
-
 .. tacn:: type of @term
 
+   This tactic returns the type of :token:`term`.
+
 Manipulating untyped terms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1041,6 +1047,7 @@ Testing boolean expressions
          Fail all:let n:= numgoals in guard n=2.
 
    .. exn:: Condition not satisfied.
+      :undocumented:
 
 Proving a subgoal as a separate lemma
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1092,6 +1099,7 @@ Proving a subgoal as a separate lemma
 
    .. exn:: Proof is not complete.
       :name: Proof is not complete. (abstract)
+      :undocumented:
 
 Tactic toplevel definitions
 ---------------------------
@@ -1348,6 +1356,6 @@ Run-time optimization tactic
 .. tacn:: optimize_heap
    :name: optimize_heap
 
-This tactic behaves like :n:`idtac`, except that running it compacts the
-heap in the OCaml run-time system. It is analogous to the Vernacular
-command :cmd:`Optimize Heap`.
+   This tactic behaves like :n:`idtac`, except that running it compacts the
+   heap in the OCaml run-time system. It is analogous to the Vernacular
+   command :cmd:`Optimize Heap`.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 0b059f92ee..590d71b5f3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -67,6 +67,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
    added to the environment as an opaque constant.
 
    .. exn:: Attempt to save an incomplete proof.
+      :undocumented:
 
    .. note::
 
@@ -106,6 +107,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
    proof was edited.
 
    .. exn:: No focused proof (No proof-editing in progress).
+      :undocumented:
 
    .. cmdv::  Abort @ident
 
@@ -282,6 +284,7 @@ Navigation in the proof tree
    This command restores the proof editing process to the original goal.
 
    .. exn:: No focused proof to restart.
+      :undocumented:
 
 .. cmd:: Focus
 
@@ -473,13 +476,14 @@ Requesting information
    This command displays the current goals.
 
    .. exn:: No focused proof.
+      :undocumented:
 
    .. cmdv:: Show @num
 
       Displays only the :token:`num`\-th subgoal.
 
       .. exn:: No such goal.
-
+         :undocumented:
 
    .. cmdv:: Show @ident
 
@@ -565,6 +569,7 @@ Requesting information
             Show Match nat.
 
       .. exn:: Unknown inductive type.
+         :undocumented:
 
    .. cmdv:: Show Universes
       :name: Show Universes
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 041f1bc966..150aadc15a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -91,6 +91,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
   of ``term``.
 
   .. 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
@@ -102,6 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
   are required.
 
   .. exn:: Not the right number of missing arguments.
+     :undocumented:
 
 .. _occurrencessets:
 
@@ -589,6 +591,7 @@ Applying theorems
       :n:`constructor 2 {? with @bindings_list }`.
 
       .. exn:: Not an inductive goal with 2 constructors.
+         :undocumented:
 
    .. tacv:: econstructor
              eexists
@@ -1081,8 +1084,8 @@ Managing the local context
       generated by Coq.
 
    .. tacv:: epose (@ident {? @binders} := @term)
-   .. tacv:: epose term
-      :name: epose
+             epose @term
+      :name: epose; _
 
       While the different variants of :tacn:`pose` expect that no
       existential variables are generated by the tactic, :tacn:`epose`
@@ -1124,7 +1127,7 @@ Managing the local context
 Controlling the proof flow
 ------------------------------
 
-.. tacn:: assert (@ident : form)
+.. tacn:: assert (@ident : @type)
    :name: assert
 
    This tactic applies to any goal. :n:`assert (H : U)` adds a new hypothesis
@@ -1132,106 +1135,104 @@ Controlling the proof flow
    :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to
    prove.
 
-.. exn:: Not a proposition or a type.
+   .. exn:: Not a proposition or a type.
 
-   Arises when the argument form is neither of type :g:`Prop`, :g:`Set` nor
-   :g:`Type`.
+      Arises when the argument :token:`type` is neither of type :g:`Prop`,
+      :g:`Set` nor :g:`Type`.
 
-.. tacv:: assert form
+   .. tacv:: assert @type
 
-   This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by
-   Coq.
+      This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is
+      generated by Coq.
 
-.. tacv:: assert @form by @tactic
+   .. tacv:: assert @type by @tactic
 
-   This tactic behaves like :n:`assert` but applies tactic to solve the subgoals
-   generated by assert.
+      This tactic behaves like :tacn:`assert` but applies tactic to solve the
+      subgoals generated by assert.
 
-   .. exn:: Proof is not complete.
-      :name: Proof is not complete. (assert)
+      .. exn:: Proof is not complete.
+         :name: Proof is not complete. (assert)
+         :undocumented:
 
-.. tacv:: assert @form as @intro_pattern
+   .. tacv:: assert @type as @intro_pattern
 
-   If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`),
-   the hypothesis is named after this introduction pattern (in particular, if
-   :n:`intro_pattern` is :n:`@ident`, the tactic behaves like
-   :n:`assert (@ident : form)`). If :n:`intro_pattern` is an action
-   introduction pattern, the tactic behaves like :n:`assert form` followed by
-   the action done by this introduction pattern.
+      If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`),
+      the hypothesis is named after this introduction pattern (in particular, if
+      :n:`intro_pattern` is :n:`@ident`, the tactic behaves like
+      :n:`assert (@ident : @type)`). If :n:`intro_pattern` is an action
+      introduction pattern, the tactic behaves like :n:`assert @type` followed by
+      the action done by this introduction pattern.
 
-.. tacv:: assert @form as @intro_pattern by @tactic
+   .. tacv:: assert @type as @intro_pattern by @tactic
 
-   This combines the two previous variants of :n:`assert`.
+      This combines the two previous variants of :tacn:`assert`.
 
-.. tacv:: assert (@ident := @term )
+   .. tacv:: assert (@ident := @term)
 
-   This behaves as :n:`assert (@ident : type) by exact @term` where :g:`type` is
-   the type of :g:`term`. This is deprecated in favor of :n:`pose proof`. If the
-   head of term is :n:`@ident`, the tactic behaves as :n:`specialize @term`.
+      This behaves as :n:`assert (@ident : @type) by exact @term` where
+      :token:`type` is the type of :token:`term`. This is equivalent to using
+      :tacn:`pose proof`. If the head of term is :token:`ident`, the tactic
+      behaves as :tacn:`specialize`.
 
-   .. exn:: Variable @ident is already declared.
+      .. exn:: Variable @ident is already declared.
+         :undocumented:
 
-.. tacv:: eassert form as intro_pattern by tactic
+.. tacv:: eassert @type as @intro_pattern by @tactic
    :name: eassert
 
-.. tacv:: assert (@ident := @term)
-
-   While the different variants of :n:`assert` expect that no existential
-   variables are generated by the tactic, :n:`eassert` removes this constraint.
+   While the different variants of :tacn:`assert` expect that no existential
+   variables are generated by the tactic, :tacn:`eassert` removes this constraint.
    This allows not to specify the asserted statement completeley before starting
    to prove it.
 
-.. tacv:: pose proof @term {? as intro_pattern}
+.. tacv:: pose proof @term {? as @intro_pattern}
    :name: pose proof
 
-   This tactic behaves like :n:`assert T {? as intro_pattern} by exact @term`
-   where :g:`T` is the type of :g:`term`. In particular,
+   This tactic behaves like :n:`assert @type {? as @intro_pattern} by exact @term`
+   where :token:`type` is the type of :token:`term`. In particular,
    :n:`pose proof @term as @ident` behaves as :n:`assert (@ident := @term)`
-   and :n:`pose proof @term as intro_pattern` is the same as applying the
-   intro_pattern to :n:`@term`.
+   and :n:`pose proof @term as @intro_pattern` is the same as applying the
+   :token:`intro_pattern` to :token:`term`.
 
-.. tacv:: epose proof term {? as intro_pattern}
+.. tacv:: epose proof @term {? as @intro_pattern}
+   :name: epose proof
 
-   While :n:`pose proof` expects that no existential variables are generated by
-   the tactic, :n:`epose proof` removes this constraint.
+   While :tacn:`pose proof` expects that no existential variables are generated by
+   the tactic, :tacn:`epose proof` removes this constraint.
 
-.. tacv:: enough (@ident : form)
+.. tacv:: enough (@ident : @type)
    :name: enough
 
-   This adds a new hypothesis of name :n:`@ident` asserting :n:`form` to the
-   goal the tactic :n:`enough` is applied to. A new subgoal stating :n:`form` is
-   inserted after the initial goal rather than before it as :n:`assert` would do.
+   This adds a new hypothesis of name :token:`ident` asserting :token:`type` to the
+   goal the tactic :tacn:`enough` is applied to. A new subgoal stating :token:`type` is
+   inserted after the initial goal rather than before it as :tacn:`assert` would do.
 
-.. tacv:: enough form
+.. tacv:: enough @type
 
-   This behaves like :n:`enough (@ident : form)` with the name :n:`@ident` of
+   This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of
    the hypothesis generated by Coq.
 
-.. tacv:: enough form as intro_pattern
+.. tacv:: enough @type as @intro_pattern
 
-   This behaves like :n:`enough form` using :n:`intro_pattern` to name or
+   This behaves like :n:`enough @type` using :token:`intro_pattern` to name or
    destruct the new hypothesis.
 
-.. tacv:: enough (@ident : @form) by @tactic
-.. tacv:: enough @form by @tactic
-.. tacv:: enough @form as @intro_pattern by @tactic
+.. tacv:: enough (@ident : @type) by @tactic
+          enough @type {? as @intro_pattern } by @tactic
 
-   This behaves as above but with :n:`tactic` expected to solve the initial goal
-   after the extra assumption :n:`form` is added and possibly destructed. If the
-   :n:`as intro_pattern` clause generates more than one subgoal, :n:`tactic` is
+   This behaves as above but with :token:`tactic` expected to solve the initial goal
+   after the extra assumption :token:`type` is added and possibly destructed. If the
+   :n:`as @intro_pattern` clause generates more than one subgoal, :token:`tactic` is
    applied to all of them.
 
-.. tacv:: eenough (@ident : form) by tactic
-   :name: eenough
-
-.. tacv:: eenough form by tactic
+.. tacv:: eenough @type {? as @intro_pattern } {? by @tactic }
+          eenough (@ident : @type) {? by @tactic }
+   :name: eenough; _
 
-.. tacv:: eenough form as intro_pattern by tactic
+   While the different variants of :tacn:`enough` expect that no existential
+   variables are generated by the tactic, :tacn:`eenough` removes this constraint.
 
-   While the different variants of :n:`enough` expect that no existential
-   variables are generated by the tactic, :n:`eenough` removes this constraint.
-
-.. tacv:: cut @form
+.. tacv:: cut @type
    :name: cut
 
    This tactic applies to any goal. It implements the non-dependent case of
@@ -1240,11 +1241,11 @@ Controlling the proof flow
    subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the
    list of remaining subgoal to prove.
 
-.. tacv:: specialize (ident {* @term}) {? as intro_pattern}
-.. tacv:: specialize ident with @bindings_list {? as intro_pattern}
-   :name: specialize
+.. tacv:: specialize (@ident {* @term}) {? as @intro_pattern}
+          specialize @ident with @bindings_list {? as @intro_pattern}
+   :name: specialize; _
 
-   The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The
+   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>`.
@@ -1254,15 +1255,18 @@ Controlling the proof flow
    uninstantiated arguments are inferred by unification if possible or left
    quantified in the hypothesis otherwise. With the :n:`as` clause, the local
    hypothesis :n:`@ident` is left unchanged and instead, the modified hypothesis
-   is introduced as specified by the :n:`intro_pattern`. The name :n:`@ident`
+   is introduced as specified by the :token:`intro_pattern`. The name :n:`@ident`
    can also refer to a global lemma or hypothesis. In this case, for
-   compatibility reasons, the behavior of :n:`specialize` is close to that of
-   :n:`generalize`: the instantiated statement becomes an additional premise of
-   the goal. The :n:`as` clause is especially useful in this case to immediately
+   compatibility reasons, the behavior of :tacn:`specialize` is close to that of
+   :tacn:`generalize`: the instantiated statement becomes an additional premise of
+   the goal. The ``as`` clause is especially useful in this case to immediately
    introduce the instantiated statement as a local hypothesis.
 
    .. exn:: @ident is used in hypothesis @ident.
+      :undocumented:
+
    .. exn:: @ident is used in conclusion.
+      :undocumented:
 
 .. tacn:: generalize @term
    :name: generalize
@@ -1343,8 +1347,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
    changes in the goal, its use is strongly discouraged.
 
 .. tacv:: instantiate ( @num := @term ) in @ident
-.. tacv:: instantiate ( @num := @term ) in ( value of @ident )
-.. tacv:: instantiate ( @num := @term ) in ( type of @ident )
+          instantiate ( @num := @term ) in ( value of @ident )
+          instantiate ( @num := @term ) in ( type of @ident )
 
    These allow to refer respectively to existential variables occurring in a
    hypothesis or in the body or the type of a local definition.
@@ -1360,13 +1364,13 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
 .. tacn:: admit
    :name: admit
 
-The admit tactic allows temporarily skipping a subgoal so as to
-progress further in the rest of the proof. A proof containing admitted
-goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
+   This tactic allows temporarily skipping a subgoal so as to
+   progress further in the rest of the proof. A proof containing admitted
+   goals cannot be closed with :cmd:`Qed` but only with :cmd:`Admitted`.
 
 .. tacv:: give_up
 
-   Synonym of :n:`admit`.
+   Synonym of :tacn:`admit`.
 
 .. tacn:: absurd @term
    :name: absurd
@@ -1387,7 +1391,8 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
    a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory
    hypotheses.
 
-.. exn:: No such assumption.
+   .. exn:: No such assumption.
+      :undocumented:
 
 .. tacv:: contradiction @ident
 
@@ -1602,6 +1607,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       induction n.
 
 .. exn:: Not an inductive product.
+   :undocumented:
 
 .. exn:: Unable to find an instance for the variables @ident ... @ident.
 
@@ -1672,10 +1678,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
          Show 2.
 
 .. tacv:: induction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences
+          einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences
 
-.. tacv:: einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences
-
-   These are the most general forms of ``induction`` and ``einduction``. It combines the
+   These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the
    effects of the with, as, using, and in clauses.
 
 .. tacv:: elim @term
@@ -1709,7 +1714,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    existential variables to be resolved later on.
 
 .. tacv:: elim @term using @term
-.. tacv:: elim @term using @term with @bindings_list
+          elim @term using @term with @bindings_list
 
    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
@@ -1717,15 +1722,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    :n:`@term`.
 
 .. tacv:: elim @term with @bindings_list using @term with @bindings_list
-.. tacv:: eelim @term with @bindings_list using @term with @bindings_list
+          eelim @term with @bindings_list using @term with @bindings_list
 
-   These are the most general forms of ``elim`` and ``eelim``. It combines the
+   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.
 
-.. tacv:: elimtype @form
+.. tacv:: elimtype @type
    :name: elimtype
 
-   The argument :n:`form` must be inductively defined. :n:`elimtype I` is
+   The argument :token:`type` must be inductively defined. :n:`elimtype I` is
    equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the
    hypothesis :g:`Hn` will not appear in the context(s) of the subgoal(s).
    Conversely, if :g:`t` is a :n:`@term` of (inductive) type :g:`I` that does
@@ -1879,7 +1884,10 @@ and an explanation of the underlying technique.
 .. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion`
 
 .. exn:: Cannot find induction information on @qualid.
+   :undocumented:
+
 .. exn:: Not the right number of induction arguments.
+   :undocumented:
 
 .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list
 
@@ -1913,7 +1921,10 @@ and an explanation of the underlying technique.
    :n:`intros until @ident`.
 
 .. exn:: No primitive equality found.
+   :undocumented:
+
 .. exn:: Not a discriminable equality.
+   :undocumented:
 
 .. tacv:: discriminate @num
 
@@ -1927,11 +1938,11 @@ and an explanation of the underlying technique.
    bindings to instantiate parameters or hypotheses of :n:`@term`.
 
 .. tacv:: ediscriminate @num
-.. tacv:: ediscriminate @term {? with @bindings_list}
-   :name: ediscriminate
+          ediscriminate @term {? with @bindings_list}
+   :name: ediscriminate; _
 
-   This works the same as ``discriminate`` but if the type of :n:`@term`, or the
-   type of the hypothesis referred to by :n:`@num`, has uninstantiated
+   This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the
+   type of the hypothesis referred to by :token:`num`, has uninstantiated
    parameters, these parameters are left as existential variables.
 
 .. tacv:: discriminate
@@ -1942,6 +1953,7 @@ and an explanation of the underlying technique.
    :n:`intro @ident; discriminate @ident`.
 
    .. exn:: No discriminable equalities.
+      :undocumented:
 
 .. tacn:: injection @term
    :name: injection
@@ -1994,9 +2006,16 @@ and an explanation of the underlying technique.
       context using :n:`intros until @ident`.
 
    .. exn:: Not a projectable equality but a discriminable one.
-   .. exn:: Nothing to do, it is an equality between convertible @terms.
+      :undocumented:
+
+   .. exn:: Nothing to do, it is an equality between convertible terms.
+      :undocumented:
+
    .. exn:: Not a primitive equality.
+      :undocumented:
+
    .. exn:: Nothing to inject.
+      :undocumented:
 
    .. tacv:: injection @num
 
@@ -2010,8 +2029,8 @@ and an explanation of the underlying technique.
       instantiate parameters or hypotheses of :n:`@term`.
 
    .. tacv:: einjection @num
-      :name: einjection
-   .. tacv:: einjection @term {? with @bindings_list}
+             einjection @term {? with @bindings_list}
+      :name: einjection; _
 
       This works the same as :n:`injection` but if the type of :n:`@term`, or the
       type of the hypothesis referred to by :n:`@num`, has uninstantiated
@@ -2023,21 +2042,22 @@ and an explanation of the underlying technique.
       :n:`intro @ident; injection @ident`.
 
       .. exn:: goal does not satisfy the expected preconditions.
+         :undocumented:
 
    .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern}
-   .. tacv:: injection @num as {+ intro_pattern}
-   .. tacv:: injection as {+ intro_pattern}
-   .. tacv:: einjection @term {? with @bindings_list} as {+ intro_pattern}
-   .. tacv:: einjection @num as {+ intro_pattern}
-   .. tacv:: einjection as {+ intro_pattern}
-
-   These variants apply :n:`intros {+ @intro_pattern}` after the call to
-   :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in
-   the context of hypotheses. The number of :n:`@intro_pattern` must not exceed
-   the number of equalities newly generated. If it is smaller, fresh
-   names are automatically generated to adjust the list of :n:`@intro_pattern`
-   to the number of new equalities. The original equality is erased if it
-   corresponds to a hypothesis.
+             injection @num as {+ intro_pattern}
+             injection as {+ intro_pattern}
+             einjection @term {? with @bindings_list} as {+ intro_pattern}
+             einjection @num as {+ intro_pattern}
+             einjection as {+ intro_pattern}
+
+      These variants apply :n:`intros {+ @intro_pattern}` after the call to
+      :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in
+      the context of hypotheses. The number of :n:`@intro_pattern` must not exceed
+      the number of equalities newly generated. If it is smaller, fresh
+      names are automatically generated to adjust the list of :n:`@intro_pattern`
+      to the number of new equalities. The original equality is erased if it
+      corresponds to a hypothesis.
 
    .. flag:: Structural Injection
 
@@ -2444,8 +2464,10 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    subgoals.
 
    .. exn:: The @term provided does not end with an equation.
+      :undocumented:
 
    .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
+      :undocumented:
 
    .. tacv:: rewrite -> @term
 
@@ -2522,6 +2544,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`.
 
    .. exn:: Terms do not have convertible types.
+      :undocumented:
 
    .. tacv:: replace @term with @term’ by @tactic
 
@@ -2544,8 +2567,8 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       the form :n:`@term’ = @term`
 
    .. tacv:: replace @term {? with @term} in clause {? by @tactic}
-   .. tacv:: replace -> @term in clause
-   .. tacv:: replace <- @term in clause
+             replace -> @term in clause
+             replace <- @term in clause
 
       Acts as before but the replacements take place in the specified clause (see
       :ref:`performingcomputations`) and not only in the conclusion of the goal. The
@@ -2658,6 +2681,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    convertible.
 
    .. exn:: Not convertible.
+      :undocumented:
 
    .. tacv:: change @term with @term’
 
@@ -2670,6 +2694,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible.
 
       .. exn:: Too few occurrences.
+         :undocumented:
 
    .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident
 
@@ -2712,12 +2737,9 @@ following:
 For backward compatibility, the notation :n:`in {+ @ident}` performs
 the conversion in hypotheses :n:`{+ @ident}`.
 
-.. tacn:: cbv {* flag}
-   :name: cbv
-.. tacn:: lazy {* flag}
-   :name: lazy
-.. tacn:: compute
-   :name: compute
+.. tacn:: cbv {* @flag}
+          lazy {* @flag}
+   :name: cbv; lazy
 
    These parameterized reduction tactics apply to any goal and perform
    the normalization of the goal according to the specified flags. In
@@ -2765,7 +2787,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
    evaluating purely computational expressions (i.e. with little dead code).
 
 .. tacv:: compute
-.. tacv:: cbv
+          cbv
+   :name: compute; _
 
    These are synonyms for ``cbv beta delta iota zeta``.
 
@@ -2774,17 +2797,17 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This is a synonym for ``lazy beta delta iota zeta``.
 
 .. tacv:: compute {+ @qualid}
-.. tacv:: cbv {+ @qualid}
+          cbv {+ @qualid}
 
    These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`.
 
 .. tacv:: compute -{+ @qualid}
-.. tacv:: cbv -{+ @qualid}
+          cbv -{+ @qualid}
 
    These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`.
 
 .. tacv:: lazy {+ @qualid}
-.. tacv:: lazy -{+ @qualid}
+          lazy -{+ @qualid}
 
    These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta`
    and :n:`lazy beta delta -{+ @qualid} iota zeta`.
@@ -2864,9 +2887,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
  on transparency and opacity).
 
 .. tacn:: cbn
-   :name: cbn
-.. tacn:: simpl
-   :name: simpl
+          simpl
+   :name: cbn; simpl
 
    These tactics apply to any goal. They try to reduce a term to
    something still readable instead of fully normalizing it. They perform
@@ -2962,7 +2984,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :g:`succ t` is reduced to :g:`S t`.
 
 .. tacv:: cbn {+ @qualid}
-.. tacv:: cbn -{+ @qualid}
+          cbn -{+ @qualid}
 
    These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta`
    and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`).
@@ -2978,16 +3000,17 @@ the conversion in hypotheses :n:`{+ @ident}`.
    matching :n:`@pattern` in the current goal.
 
    .. exn:: Too few occurrences.
+      :undocumented:
 
 .. tacv:: simpl @qualid
-.. tacv:: simpl @string
+          simpl @string
 
-   This applies ``simpl`` only to the applicative subterms whose head occurrence
+   This applies :tacn:`simpl` only to the applicative subterms whose head occurrence
    is the unfoldable constant :n:`@qualid` (the constant can be referred to by
    its notation using :n:`@string` if such a notation exists).
 
 .. tacv:: simpl @qualid at {+ @num}
-.. tacv:: simpl @string at {+ @num}
+          simpl @string at {+ @num}
 
    This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
@@ -3008,6 +3031,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :math:`\beta`:math:`\iota`-normal form.
 
 .. exn:: @qualid does not denote an evaluable constant.
+   :undocumented:
 
 .. tacv:: unfold @qualid in @ident
 
@@ -3025,8 +3049,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
    unfolded. Occurrences are located from left to right.
 
    .. exn:: Bad occurrence number of @qualid.
+      :undocumented:
 
    .. exn:: @qualid does not occur.
+      :undocumented:
 
 .. tacv:: unfold @string
 
@@ -3117,6 +3143,7 @@ Conversion tactics applied to hypotheses
    Example: :n:`unfold not in (type of H1) (type of H3)`.
 
 .. exn:: No such hypothesis: @ident.
+   :undocumented:
 
 
 .. _automation:
@@ -3127,38 +3154,41 @@ Automation
 .. tacn:: auto
    :name: auto
 
-This tactic implements a Prolog-like resolution procedure to solve the
-current goal. It first tries to solve the goal using the assumption
-tactic, then it reduces the goal to an atomic one using intros and
-introduces the newly generated hypotheses as hints. Then it looks at
-the list of tactics associated to the head symbol of the goal and
-tries to apply one of them (starting from the tactics with lower
-cost). This process is recursively applied to the generated subgoals.
+   This tactic implements a Prolog-like resolution procedure to solve the
+   current goal. It first tries to solve the goal using the assumption
+   tactic, then it reduces the goal to an atomic one using intros and
+   introduces the newly generated hypotheses as hints. Then it looks at
+   the list of tactics associated to the head symbol of the goal and
+   tries to apply one of them (starting from the tactics with lower
+   cost). This process is recursively applied to the generated subgoals.
 
-By default, auto only uses the hypotheses of the current goal and the
-hints of the database named core.
+   By default, auto only uses the hypotheses of the current goal and the
+   hints of the database named core.
 
 .. tacv:: auto @num
 
-  Forces the search depth to be :n:`@num`. The maximal search depth
-  is `5` by default.
+   Forces the search depth to be :token:`num`. The maximal search depth
+   is 5 by default.
 
 .. tacv:: auto with {+ @ident}
 
-  Uses the hint databases :n:`{+ @ident}` in addition to the database core. See
-  :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of
-  pre-defined databases and the way to create or extend a database.
+   Uses the hint databases :n:`{+ @ident}` in addition to the database core.
+
+   .. seealso::
+      :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of
+      pre-defined databases and the way to create or extend a database.
 
 .. tacv:: auto with *
 
-  Uses all existing hint databases. See
-  :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
+   Uses all existing hint databases.
+
+   .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
-.. tacv:: auto using {+ @lemma}
+.. tacv:: auto using {+ @ident__i} {? with {+ @ident } }
 
-  Uses :n:`{+ @lemma}` in addition to hints (can be combined with the with
-  :n:`@ident` option).  If :n:`@lemma` is an inductive type, it is the
-  collection of its constructors which is added as hints.
+   Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an
+   inductive type, it is the collection of its constructors which are added
+   as hints.
 
 .. tacv:: info_auto
 
@@ -3184,13 +3214,24 @@ hints of the database named core.
    equalities like :g:`X=X`.
 
 .. tacv:: trivial with {+ @ident}
+   :undocumented:
+
 .. tacv:: trivial with *
+   :undocumented:
+
 .. tacv:: trivial using {+ @lemma}
+   :undocumented:
+
 .. tacv:: debug trivial
    :name: debug trivial
+   :undocumented:
+
 .. tacv:: info_trivial
    :name: info_trivial
+   :undocumented:
+
 .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}}
+   :undocumented:
 
 .. note::
   :tacn:`auto` either solves completely the goal or else leaves it
@@ -3210,26 +3251,26 @@ the :tacn:`auto` and :tacn:`trivial` tactics:
 .. tacn:: eauto
    :name: eauto
 
-This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try
-resolution hints which would leave existential variables in the goal,
-:tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply`
-where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto`
-can solve such a goal:
+   This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try
+   resolution hints which would leave existential variables in the goal,
+   :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply`
+   where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto`
+   can solve such a goal:
 
-.. example::
+   .. example::
 
-   .. coqtop:: all
+      .. coqtop:: all
 
-      Hint Resolve ex_intro.
-      Goal forall P:nat -> Prop, P 0 -> exists n, P n.
-      eauto.
+         Hint Resolve ex_intro.
+         Goal forall P:nat -> Prop, P 0 -> exists n, P n.
+         eauto.
 
-Note that ``ex_intro`` should be declared as a hint.
+      Note that ``ex_intro`` should be declared as a hint.
 
 
 .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}}
 
-  The various options for eauto are the same as for auto.
+   The various options for :tacn:`eauto` are the same as for :tacn:`auto`.
 
 :tacn:`eauto` also obeys the following options:
 
@@ -3243,13 +3284,12 @@ Note that ``ex_intro`` should be declared as a hint.
 .. tacn:: autounfold with {+ @ident}
    :name: autounfold
 
-
-This tactic unfolds constants that were declared through a ``Hint Unfold``
-in the given databases.
+   This tactic unfolds constants that were declared through a :cmd:`Hint Unfold`
+   in the given databases.
 
 .. tacv:: autounfold with {+ @ident} in clause
 
-  Performs the unfolding in the given clause.
+   Performs the unfolding in the given clause.
 
 .. tacv:: autounfold with *
 
@@ -3258,18 +3298,18 @@ in the given databases.
 .. tacn:: autorewrite with {+ @ident}
    :name: autorewrite
 
-This tactic [4]_ carries out rewritings according to the rewriting rule
-bases :n:`{+ @ident}`.
+   This tactic [4]_ carries out rewritings according to the rewriting rule
+   bases :n:`{+ @ident}`.
 
-Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
-it fails. Once all the rules have been processed, if the main subgoal has
-progressed (e.g., if it is distinct from the initial main goal) then the rules
-of this base are processed again. If the main subgoal has not progressed then
-the next base is processed. For the bases, the behavior is exactly similar to
-the processing of the rewriting rules.
+   Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
+   it fails. Once all the rules have been processed, if the main subgoal has
+   progressed (e.g., if it is distinct from the initial main goal) then the rules
+   of this base are processed again. If the main subgoal has not progressed then
+   the next base is processed. For the bases, the behavior is exactly similar to
+   the processing of the rewriting rules.
 
-The rewriting rule bases are built with the ``Hint Rewrite vernacular``
-command.
+   The rewriting rule bases are built with the :cmd:`Hint Rewrite`
+   command.
 
 .. warning::
 
@@ -3435,6 +3475,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       itself.
 
    .. exn:: @term cannot be used as a hint
+      :undocumented:
 
    .. cmdv:: Immediate {+ @term}
 
@@ -3448,6 +3489,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor.
 
    .. exn:: @ident is not an inductive type
+      :undocumented:
 
    .. cmdv:: Hint Constructors {+ @ident}
 
@@ -3616,16 +3658,16 @@ use one or several databases specific to your development.
 
 .. cmd:: Remove Hints {+ @term} : {+ @ident}
 
-This command removes the hints associated to terms :n:`{+ @term}` in databases
-:n:`{+ @ident}`.
+   This command removes the hints associated to terms :n:`{+ @term}` in databases
+   :n:`{+ @ident}`.
 
 .. _printhint:
 
 .. cmd:: Print Hint
 
-This command displays all hints that apply to the current goal. It
-fails if no proof is being edited, while the two variants can be used
-at every moment.
+   This command displays all hints that apply to the current goal. It
+   fails if no proof is being edited, while the two variants can be used
+   at every moment.
 
 **Variants:**
 
@@ -3753,17 +3795,17 @@ Decision procedures
 .. tacn:: tauto
    :name: tauto
 
-This tactic implements a decision procedure for intuitionistic propositional
-calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
-:cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an
-intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and
-logical equivalence but does not unfold any other definition.
-
-The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
-fail:
+   This tactic implements a decision procedure for intuitionistic propositional
+   calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
+   :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an
+   intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and
+   logical equivalence but does not unfold any other definition.
 
 .. example::
 
+   The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
+   fail:
+
    .. coqtop:: reset all
 
       Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
@@ -3799,27 +3841,24 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
 .. tacn:: intuition @tactic
    :name: intuition
 
-The tactic :tacn:`intuition` takes advantage of the search-tree built by the
-decision procedure involved in the tactic :tacn:`tauto`. It uses this
-information to generate a set of subgoals equivalent to the original one (but
-simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If
-this tactic fails on some goals then :tacn:`intuition` fails. In fact,
-:tacn:`tauto` is simply :g:`intuition fail`.
+   The tactic :tacn:`intuition` takes advantage of the search-tree built by the
+   decision procedure involved in the tactic :tacn:`tauto`. It uses this
+   information to generate a set of subgoals equivalent to the original one (but
+   simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If
+   this tactic fails on some goals then :tacn:`intuition` fails. In fact,
+   :tacn:`tauto` is simply :g:`intuition fail`.
 
-For instance, the tactic :g:`intuition auto` applied to the goal
-
-::
-
-    (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O
+   .. example::
 
+      For instance, the tactic :g:`intuition auto` applied to the goal::
 
-internally replaces it by the equivalent one:
-::
+         (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O
 
-    (forall (x:nat), P x), B |- P O
+      internally replaces it by the equivalent one::
 
+        (forall (x:nat), P x), B |- P O
 
-and then uses :tacn:`auto` which completes the proof.
+      and then uses :tacn:`auto` which completes the proof.
 
 Originally due to César Muñoz, these tactics (:tacn:`tauto` and
 :tacn:`intuition`) have been completely re-engineered by David Delahaye using
@@ -3849,25 +3888,25 @@ some incompatibilities.
 .. tacn:: rtauto
    :name: rtauto
 
-The :tacn:`rtauto` tactic solves propositional tautologies similarly to what
-:tacn:`tauto` does. The main difference is that the proof term is built using a
-reflection scheme applied to a sequent calculus proof of the goal.  The search
-procedure is also implemented using a different technique.
+   The :tacn:`rtauto` tactic solves propositional tautologies similarly to what
+   :tacn:`tauto` does. The main difference is that the proof term is built using a
+   reflection scheme applied to a sequent calculus proof of the goal.  The search
+   procedure is also implemented using a different technique.
 
-Users should be aware that this difference may result in faster proof-search
-but slower proof-checking, and :tacn:`rtauto` might not solve goals that
-:tacn:`tauto` would be able to solve (e.g. goals involving universal
-quantifiers).
+   Users should be aware that this difference may result in faster proof-search
+   but slower proof-checking, and :tacn:`rtauto` might not solve goals that
+   :tacn:`tauto` would be able to solve (e.g. goals involving universal
+   quantifiers).
 
-Note that this tactic is only available after a ``Require Import Rtauto``.
+   Note that this tactic is only available after a ``Require Import Rtauto``.
 
 .. tacn:: firstorder
    :name: firstorder
 
-The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to
-first- order reasoning, written by Pierre Corbineau. It is not restricted to
-usual logical connectives but instead may reason about any first-order class
-inductive definition.
+   The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to
+   first- order reasoning, written by Pierre Corbineau. It is not restricted to
+   usual logical connectives but instead may reason about any first-order class
+   inductive definition.
 
 .. opt:: Firstorder Solver @tactic
    :name: Firstorder Solver
@@ -3906,20 +3945,20 @@ inductive definition.
 .. tacn:: congruence
    :name: congruence
 
-The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard
-Nelson and Oppen congruence closure algorithm, which is a decision procedure
-for ground equalities with uninterpreted symbols. It also includes
-constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal
-is a non-quantified equality, congruence tries to prove it with non-quantified
-equalities in the context. Otherwise it tries to infer a discriminable equality
-from those in the context. Alternatively, congruence tries to prove that a
-hypothesis is equal to the goal or to the negation of another hypothesis.
-
-:tacn:`congruence` is also able to take advantage of hypotheses stating
-quantified equalities, but you have to provide a bound for the number of extra
-equalities generated that way. Please note that one of the sides of the
-equality must contain all the quantified variables in order for congruence to
-match against it.
+   The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard
+   Nelson and Oppen congruence closure algorithm, which is a decision procedure
+   for ground equalities with uninterpreted symbols. It also includes
+   constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal
+   is a non-quantified equality, congruence tries to prove it with non-quantified
+   equalities in the context. Otherwise it tries to infer a discriminable equality
+   from those in the context. Alternatively, congruence tries to prove that a
+   hypothesis is equal to the goal or to the negation of another hypothesis.
+
+   :tacn:`congruence` is also able to take advantage of hypotheses stating
+   quantified equalities, but you have to provide a bound for the number of extra
+   equalities generated that way. Please note that one of the sides of the
+   equality must contain all the quantified variables in order for congruence to
+   match against it.
 
 .. example::
 
@@ -3980,7 +4019,10 @@ succeeds, and results in an error otherwise.
    conversion, casts and universe constraints. It may unify universes.
 
 .. exn:: Not equal.
+   :undocumented:
+
 .. exn:: Not equal (due to universes).
+   :undocumented:
 
 .. tacn:: constr_eq_strict @term @term
    :name: constr_eq_strict
@@ -3990,7 +4032,10 @@ succeeds, and results in an error otherwise.
    constraints.
 
 .. exn:: Not equal.
+   :undocumented:
+
 .. exn:: Not equal (due to universes).
+   :undocumented:
 
 .. tacn:: unify @term @term
    :name: unify
@@ -3999,6 +4044,7 @@ succeeds, and results in an error otherwise.
    instantiating existential variables.
 
 .. exn:: Unable to unify @term with @term.
+   :undocumented:
 
 .. tacv:: unify @term @term with @ident
 
@@ -4013,6 +4059,7 @@ succeeds, and results in an error otherwise.
    by :tacn:`eapply` and some other tactics.
 
 .. exn:: Not an evar.
+   :undocumented:
 
 .. tacn:: has_evar @term
    :name: has_evar
@@ -4022,6 +4069,7 @@ succeeds, and results in an error otherwise.
    scans all subterms, including those under binders.
 
 .. exn:: No evars.
+   :undocumented:
 
 .. tacn:: is_var @term
    :name: is_var
@@ -4030,6 +4078,7 @@ succeeds, and results in an error otherwise.
    the current goal context or in the opened sections.
 
 .. exn:: Not a variable or hypothesis.
+   :undocumented:
 
 
 .. _equality:
@@ -4041,45 +4090,46 @@ Equality
 .. tacn:: f_equal
    :name: f_equal
 
-This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n`
-:g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`.  Using :tacn:`f_equal` on such a goal
-leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up
-to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones
-(e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically
-solved by :tacn:`f_equal`.
+   This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n`
+   :g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`.  Using :tacn:`f_equal` on such a goal
+   leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up
+   to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones
+   (e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically
+   solved by :tacn:`f_equal`.
 
 
 .. tacn:: reflexivity
    :name: reflexivity
 
-This tactic applies to a goal that has the form :g:`t=u`. It checks that `t`
-and `u` are convertible and then solves the goal. It is equivalent to
-``apply refl_equal``.
+   This tactic applies to a goal that has the form :g:`t=u`. It checks that `t`
+   and `u` are convertible and then solves the goal. It is equivalent to
+   ``apply refl_equal``.
 
-.. exn:: The conclusion is not a substitutive equation.
+   .. exn:: The conclusion is not a substitutive equation.
+      :undocumented:
 
-.. exn:: Unable to unify ... with ...
+   .. exn:: Unable to unify ... with ...
+      :undocumented:
 
 
 .. tacn:: symmetry
    :name: symmetry
 
-This tactic applies to a goal that has the form :g:`t=u` and changes it into
-:g:`u=t`.
+   This tactic applies to a goal that has the form :g:`t=u` and changes it into
+   :g:`u=t`.
 
 
 .. tacv:: symmetry in @ident
 
-  If the statement of the hypothesis ident has the form :g:`t=u`, the tactic
-  changes it to :g:`u=t`.
-
+   If the statement of the hypothesis ident has the form :g:`t=u`, the tactic
+   changes it to :g:`u=t`.
 
 
 .. tacn:: transitivity @term
    :name: transitivity
 
-This tactic applies to a goal that has the form :g:`t=u` and transforms it
-into the two subgoals :n:`t=@term` and :n:`@term=u`.
+   This tactic applies to a goal that has the form :g:`t=u` and transforms it
+   into the two subgoals :n:`t=@term` and :n:`@term=u`.
 
 
 Equality and inductive sets
@@ -4133,10 +4183,10 @@ symbol :g:`=`.
    instantiate parameters or hypotheses of :n:`@term`.
 
 .. tacv:: esimplify_eq @num
-.. tacv:: esimplify_eq @term {? with @bindings_list}
-   :name: esimplify_eq
+          esimplify_eq @term {? with @bindings_list}
+   :name: esimplify_eq; _
 
-   This works the same as ``simplify_eq`` but if the type of :n:`@term`, or the
+   This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the
    type of the hypothesis referred to by :n:`@num`, has uninstantiated
    parameters, these parameters are left as existential variables.
 
@@ -4168,35 +4218,35 @@ Inversion
 .. tacn:: functional inversion @ident
    :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 Function (see
-:ref:`advanced-recursive-functions`). Note that this tactic is only
-available after a ``Require Import FunInd``.
+   :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 Function (see
+   :ref:`advanced-recursive-functions`). Note that this tactic is only
+   available after a ``Require Import FunInd``.
 
+   .. exn:: Hypothesis @ident must contain at least one Function.
+      :undocumented:
 
-.. exn:: Hypothesis @ident must contain at least one Function.
-.. exn:: Cannot find inversion information for hypothesis @ident.
+   .. exn:: Cannot find inversion information for hypothesis @ident.
 
-  This error may be raised when some inversion lemma failed to be generated by
-  Function.
+      This error may be raised when some inversion lemma failed to be generated by
+      Function.
 
 
-.. tacv:: functional inversion @num
+   .. tacv:: functional inversion @num
 
-  This does the same thing as :n:`intros until @num` folowed by
-  :n:`functional inversion @ident` where :token:`ident` is the
-  identifier for the last introduced hypothesis.
+      This does the same thing as :n:`intros until @num` folowed by
+      :n:`functional inversion @ident` where :token:`ident` is the
+      identifier for the last introduced hypothesis.
 
-.. tacv:: functional inversion ident qualid
-.. tacv:: functional inversion num qualid
+   .. tacv:: functional inversion @ident @qualid
+             functional inversion @num @qualid
 
-  If the hypothesis :n:`@ident` (or :n:`@num`) has a type of the form
-  :n:`@qualid`:sub:`1` :n:`@term`:sub:`1` ... :n:`@term`:sub:`n` :n:`=
-  @qualid`:sub:`2` :n:`@term`:sub:`n+1` ... :n:`@term`:sub:`n+m` where
-  :n:`@qualid`:sub:`1` and :n:`@qualid`:sub:`2` are valid candidates to
-  functional inversion, this variant allows choosing which :n:`@qualid` is
-  inverted.
+      If the hypothesis :token:`ident` (or :token:`num`) 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.
 
 Classical tactics
 -----------------
@@ -4206,15 +4256,14 @@ loaded. A few more tactics are available. Make sure to load the module
 using the ``Require Import`` command.
 
 .. tacn:: classical_left
-   :name: classical_left
-.. tacv:: classical_right
-   :name: classical_right
+          classical_right
+   :name: classical_left; classical_right
 
-   The tactics ``classical_left`` and ``classical_right`` are the analog of the
-   left and right but using classical logic. They can only be used for
-   disjunctions. Use ``classical_left`` to prove the left part of the
+   These tactics are the analog of :tacn:`left` and :tacn:`right`
+   but using classical logic. They can only be used for
+   disjunctions. Use :tacn:`classical_left` to prove the left part of the
    disjunction with the assumption that the negation of right part holds.
-   Use ``classical_right`` to prove the right part of the disjunction with
+   Use :tacn:`classical_right` to prove the right part of the disjunction with
    the assumption that the negation of left part holds.
 
 .. _tactics-automating:
@@ -4226,93 +4275,92 @@ Automating
 .. tacn:: btauto
    :name: btauto
 
-The tactic :tacn:`btauto` implements a reflexive solver for boolean
-tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are
-constructed over the following grammar:
+   The tactic :tacn:`btauto` implements a reflexive solver for boolean
+   tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are
+   constructed over the following grammar:
 
-.. _btauto_grammar:
+   .. _btauto_grammar:
 
-  .. productionlist:: `sentence`
-     t : x
-       :∣ true
-       :∣ false
-       :∣ orb t1 t2
-       :∣ andb t1 t2
-       :∣ xorb t1 t2
-       :∣ negb t
-       :∣ if t1 then t2 else t3
+   .. productionlist:: `sentence`
+      t : x
+        :∣ true
+        :∣ false
+        :∣ orb t1 t2
+        :∣ andb t1 t2
+        :∣ xorb t1 t2
+        :∣ negb t
+        :∣ if t1 then t2 else t3
 
-  Whenever the formula supplied is not a tautology, it also provides a
-  counter-example.
+   Whenever the formula supplied is not a tautology, it also provides a
+   counter-example.
 
-  Internally, it uses a system very similar to the one of the ring
-  tactic.
+   Internally, it uses a system very similar to the one of the ring
+   tactic.
 
-  Note that this tactic is only available after a ``Require Import Btauto``.
+   Note that this tactic is only available after a ``Require Import Btauto``.
 
-.. exn:: Cannot recognize a boolean equality.
+   .. exn:: Cannot recognize a boolean equality.
 
-   The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
-   doesn't introduce variables into the context on its own.
+      The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
+      doesn't introduce variables into the context on its own.
 
 .. tacn:: omega
    :name: omega
 
-The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision
-procedure for Presburger arithmetic. It solves quantifier-free
-formulas built with `~`, `\/`, `/\`, `->` on top of equalities,
-inequalities and disequalities on both the type :g:`nat` of natural numbers
-and :g:`Z` of binary integers. This tactic must be loaded by the command
-``Require Import Omega``. See the additional documentation about omega
-(see Chapter :ref:`omega`).
+   The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision
+   procedure for Presburger arithmetic. It solves quantifier-free
+   formulas built with `~`, `\/`, `/\`, `->` on top of equalities,
+   inequalities and disequalities on both the type :g:`nat` of natural numbers
+   and :g:`Z` of binary integers. This tactic must be loaded by the command
+   ``Require Import Omega``. See the additional documentation about omega
+   (see Chapter :ref:`omega`).
 
 
 .. tacn:: ring
    :name: ring
+
+   This tactic solves equations upon polynomial expressions of a ring
+   (or semiring) structure. It proceeds by normalizing both hand sides
+   of the equation (w.r.t. associativity, commutativity and
+   distributivity, constant propagation) and comparing syntactically the
+   results.
+
 .. tacn:: ring_simplify {+ @term}
    :name: ring_simplify
 
-The :n:`ring` tactic solves equations upon polynomial expressions of a ring
-(or semiring) structure. It proceeds by normalizing both hand sides
-of the equation (w.r.t. associativity, commutativity and
-distributivity, constant propagation) and comparing syntactically the
-results.
-
-:n:`ring_simplify` 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
-is given, then the conclusion should be an equation and both hand
-sides are normalized.
+   This tactic 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
+   is given, then the conclusion should be an equation and both hand
+   sides are normalized.
 
 See :ref:`Theringandfieldtacticfamilies` for more information on
 the tactic and how to declare new ring structures. All declared field structures
 can be printed with the ``Print Rings`` command.
 
 .. tacn:: field
-   :name: field
-.. tacn:: field_simplify {+ @term}
-   :name: field_simplify
-.. tacn:: field_simplify_eq
-   :name: field_simplify_eq
-
-The field tactic is built on the same ideas as ring: this is a
-reflexive tactic that solves or simplifies equations in a field
-structure. The main idea is to reduce a field expression (which is an
-extension of ring expressions with the inverse and division
-operations) to a fraction made of two polynomial expressions.
-
-Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}`
-replaces the provided terms by their reduced fraction.
-:n:`field_simplify_eq` applies when the conclusion is an equation: it
-simplifies both hand sides and multiplies so as to cancel
-denominators. So it produces an equation without division nor inverse.
-
-All of these 3 tactics may generate a subgoal in order to prove that
-denominators are different from zero.
-
-See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to
-declare new field structures. All declared field structures can be
-printed with the Print Fields command.
+          field_simplify {+ @term}
+          field_simplify_eq
+   :name: field; field_simplify; field_simplify_eq
+
+   The field tactic is built on the same ideas as ring: this is a
+   reflexive tactic that solves or simplifies equations in a field
+   structure. The main idea is to reduce a field expression (which is an
+   extension of ring expressions with the inverse and division
+   operations) to a fraction made of two polynomial expressions.
+
+   Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}`
+   replaces the provided terms by their reduced fraction.
+   :n:`field_simplify_eq` applies when the conclusion is an equation: it
+   simplifies both hand sides and multiplies so as to cancel
+   denominators. So it produces an equation without division nor inverse.
+
+   All of these 3 tactics may generate a subgoal in order to prove that
+   denominators are different from zero.
+
+   See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to
+   declare new field structures. All declared field structures can be
+   printed with the Print Fields command.
 
 .. example::
 
@@ -4373,16 +4421,16 @@ Non-logical tactics
 .. tacn:: revgoals
    :name: revgoals
 
-This tactics reverses the list of the focused goals.
+   This tactics reverses the list of the focused goals.
 
-.. example::
+   .. example::
 
-   .. coqtop:: all reset
+      .. coqtop:: all reset
 
-      Parameter P : nat -> Prop.
-      Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
-      repeat split.
-      all: revgoals.
+         Parameter P : nat -> Prop.
+         Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
+         repeat split.
+         all: revgoals.
 
 .. tacn:: shelve
    :name: shelve
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a69cf209c7..4bc85f386d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -20,10 +20,13 @@ Displaying
    Error messages:
 
    .. exn:: @qualid not a defined object.
+      :undocumented:
 
    .. exn:: Universe instance should have length @num.
+      :undocumented:
 
    .. exn:: This object does not support universe names.
+      :undocumented:
 
 
    .. cmdv:: Print Term @qualid
@@ -81,9 +84,9 @@ and tables:
 * A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`.
 * An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`.
 * A :production:`table` contains a set of strings or qualids.
-* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`.
+* In addition, some commands provide settings, such as :cmd:`Extraction Language`.
 
-.. FIXME Convert `Extraction Language OCaml` to an option.
+.. FIXME Convert "Extraction Language" to an option.
 
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
@@ -538,8 +541,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
       will use the default extension ``.v``.
 
    .. cmdv:: Load Verbose @ident
-
-   .. cmdv:: Load Verbose @string
+             Load Verbose @string
 
       Display, while loading,
       the answers of |Coq| to each command (including tactics) contained in
@@ -548,10 +550,13 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
       .. seealso:: Section :ref:`controlling-display`.
 
    .. exn:: Can’t find file @ident on loadpath.
+      :undocumented:
 
    .. exn:: Load is not supported inside proofs.
+      :undocumented:
 
    .. exn:: Files processed by Load cannot leave open proofs.
+      :undocumented:
 
 .. _compiled-files:
 
@@ -620,6 +625,7 @@ file is a particular case of module called *library file*.
       comes from a given package by making explicit its absolute root.
 
    .. exn:: Cannot load qualid: no physical path bound to dirpath.
+      :undocumented:
 
    .. exn:: Cannot find library foo in loadpath.
 
@@ -684,8 +690,10 @@ file is a particular case of module called *library file*.
       where they occur, even if outside a section.
 
    .. exn:: File not found on loadpath: @string.
+      :undocumented:
 
    .. exn:: Loading of ML object file forbidden in a native Coq.
+      :undocumented:
 
 
 .. cmd:: Print ML Modules
@@ -812,6 +820,7 @@ interactively, they cannot be part of a vernacular file loaded via
    over the name of a module or of an object inside a module.
 
    .. exn:: @ident: no such entry.
+      :undocumented:
 
    .. cmdv:: Reset Initial
 
@@ -953,6 +962,7 @@ Quitting and debugging
    it prints a message indicating that the failure did not occur.
 
    .. exn:: The command has not failed!
+      :undocumented:
 
 
 .. _controlling-display:
@@ -1136,6 +1146,7 @@ described first.
    variable nor a constant.
 
    .. exn:: The reference is not unfoldable.
+      :undocumented:
 
    .. cmdv:: Print Strategies
 
@@ -1166,41 +1177,41 @@ Controlling the locality of commands
 
 
 .. cmd:: Local @command
-.. cmd:: Global @command
-
-Some commands support a Local or Global prefix modifier to control the
-scope of their effect. There are four kinds of commands:
-
-
-+ Commands whose default is to extend their effect both outside the
-  section and the module or library file they occur in.  For these
-  commands, the Local modifier limits the effect of the command to the
-  current section or module it occurs in.  As an example, the :cmd:`Coercion`
-  and :cmd:`Strategy` commands belong to this category.
-+ Commands whose default behavior is to stop their effect at the end
-  of the section they occur in but to extend their effect outside the module or
-  library file they occur in. For these commands, the Local modifier limits the
-  effect of the command to the current module if the command does not occur in a
-  section and the Global modifier extends the effect outside the current
-  sections and current module if the command occurs in a section. As an example,
-  the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
-  to this category. Notice that a subclass of these commands do not support
-  extension of their scope outside sections at all and the Global modifier is not
-  applicable to them.
-+ Commands whose default behavior is to stop their effect at the end
-  of the section or module they occur in.  For these commands, the ``Global``
-  modifier extends their effect outside the sections and modules they
-  occur in.  The :cmd:`Transparent` and :cmd:`Opaque`
-  (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands
-  belong to this category.
-+ Commands whose default behavior is to extend their effect outside
-  sections but not outside modules when they occur in a section and to
-  extend their effect outside the module or library file they occur in
-  when no section contains them.For these commands, the Local modifier
-  limits the effect to the current section or module while the Global
-  modifier extends the effect outside the module even when the command
-  occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
-  category.
+         Global @command
+
+   Some commands support a Local or Global prefix modifier to control the
+   scope of their effect. There are four kinds of commands:
+
+
+   + Commands whose default is to extend their effect both outside the
+     section and the module or library file they occur in.  For these
+     commands, the Local modifier limits the effect of the command to the
+     current section or module it occurs in.  As an example, the :cmd:`Coercion`
+     and :cmd:`Strategy` commands belong to this category.
+   + Commands whose default behavior is to stop their effect at the end
+     of the section they occur in but to extend their effect outside the module or
+     library file they occur in. For these commands, the Local modifier limits the
+     effect of the command to the current module if the command does not occur in a
+     section and the Global modifier extends the effect outside the current
+     sections and current module if the command occurs in a section. As an example,
+     the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
+     to this category. Notice that a subclass of these commands do not support
+     extension of their scope outside sections at all and the Global modifier is not
+     applicable to them.
+   + Commands whose default behavior is to stop their effect at the end
+     of the section or module they occur in.  For these commands, the ``Global``
+     modifier extends their effect outside the sections and modules they
+     occur in.  The :cmd:`Transparent` and :cmd:`Opaque`
+     (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands
+     belong to this category.
+   + Commands whose default behavior is to extend their effect outside
+     sections but not outside modules when they occur in a section and to
+     extend their effect outside the module or library file they occur in
+     when no section contains them.For these commands, the Local modifier
+     limits the effect to the current section or module while the Global
+     modifier extends the effect outside the module even when the command
+     occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
+     category.
 
 .. _exposing-constants-to-ocaml-libraries:
 
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 8f76085d88..418922e9b3 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -12,7 +12,7 @@ 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__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j Sort sort}
+.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort @sort {* with @ident__i := Induction for @ident__j Sort @sort}
 
   This command is a high-level tool for generating automatically
   (possibly mutual) induction principles for given types and sorts.
@@ -22,10 +22,10 @@ syntax follows the schema:
   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}
+.. 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.
+   Same as before but defines a non-dependent elimination principle more
+   natural in case of inductively defined relations.
 
 .. cmdv:: Scheme Equality for @ident
    :name: Scheme Equality
@@ -33,7 +33,7 @@ syntax follows the schema:
    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.
 
-.. cmdv:: Scheme Induction for @ident Sort sort {* with Induction for @ident Sort sort}
+.. 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).
@@ -195,19 +195,18 @@ Combined Scheme
 Generation of induction principles with ``Functional`` ``Scheme``
 -----------------------------------------------------------------
 
-The ``Functional Scheme`` 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``. Its syntax then follows the
-schema:
 
-.. cmd:: Functional Scheme @ident := Induction for ident' Sort sort {* with @ident := Induction for @ident Sort sort}
+.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort}
 
-where each `ident'ᵢ` 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 `identᵢ`, following
-the recursive structure and case analyses of the corresponding function
-identᵢ’.
+   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'`.
 
 .. warning::
 
@@ -349,17 +348,17 @@ Generation of inversion principles with ``Derive`` ``Inversion``
    :g:`inversion`.
 
 
-.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort
+.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort
 
    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 forall (x:T), I t Sort sort
+.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort
 
    When applied, it is equivalent to having inverted the instance with
    the tactic `dependent inversion`.
 
-.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort sort
+.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort
 
    When applied, it is equivalent to having inverted the instance
    with the tactic `dependent inversion_clear`.
@@ -377,8 +376,8 @@ Generation of inversion principles with ``Derive`` ``Inversion``
 
     Parameter P : nat -> nat -> Prop.
 
-  To generate the inversion lemma for the instance `(Le (S n) m)` and the
-  sort `Prop`, we do:
+  To generate the inversion lemma for the instance :g:`(Le (S n) m)` and the
+  sort :g:`Prop`, we do:
 
   .. coqtop:: all
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 2214cbfb34..65df89da6c 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -31,8 +31,8 @@ Basic notations
 
 .. cmd:: Notation
 
-A *notation* is a symbolic expression denoting some term or term
-pattern.
+   A *notation* is a symbolic expression denoting some term or term
+   pattern.
 
 A typical notation is the use of the infix symbol ``/\`` to denote the
 logical conjunction (and). Such a notation is declared by