Merge PR #9036: Add bodies to sphinx objects.

9 files changed, 263 insertions, 248 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