[Sphinx] Clean-up indices

5 files changed, 83 insertions, 73 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index d60387f4f..e4dea3487 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -537,14 +537,19 @@ 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 [in @ident] [using relation @term] [by @tactic]
+   :name: setoid_replace
 
 
 The ``using relation`` arguments cannot be passed to the unprefixed form.
@@ -583,7 +588,7 @@ Deprecated syntax and backward incompatibilities
 Due to backward compatibility reasons, the following syntax for the
 declaration of setoids and morphisms is also accepted.
 
-.. tacv:: Add Setoid @A @Aeq @ST as @ident
+.. cmd:: Add Setoid @A @Aeq @ST as @ident
 
 where ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier
 and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record
@@ -818,7 +823,8 @@ Usage
 ~~~~~
 
 
-.. tacv:: rewrite_strat @s [in @ident]
+.. tacn:: rewrite_strat @s [in @ident]
+   :name: rewrite_strat
 
    Rewrite using the strategy s in hypothesis ident or the conclusion.
 
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 19d4ba9ba..c48c2d7ce 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -138,7 +138,7 @@ Declaration of Coercions
   .. exn:: @qualid does not respect the uniform inheritance condition
   .. exn:: Found target class ... instead of ...
 
-  .. warn:: Ambigous path:
+  .. warn:: Ambiguous path
 
     When the coercion `qualid` is added to the inheritance graph, non
     valid coercion paths are ignored; they are signaled by a warning
@@ -218,6 +218,7 @@ declaration, this constructor is declared as a coercion.
     Idem but locally to the current section.
 
   .. cmdv:: SubClass @ident := @type.
+     :name: SubClass
 
     If `type` is a class `ident'` applied to some arguments then
     `ident` is defined and an identity coercion of name
@@ -291,6 +292,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is:
    satisfied).
 
 .. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
+   :name: Structure
 
    This is a synonym of :cmd:`Record`.
 
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index e850587c8..4f8cc34d4 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -13,20 +13,19 @@ tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`
 It also possible to get the tactics for integers by a ``Require Import Lia``,
 rationals ``Require Import Lqa`` and reals ``Require Import Lra``.
 
-+ ``lia`` is a decision procedure for linear integer arithmetic (see Section :ref:`lia <lia>`);
-+ ``nia`` is an incomplete proof procedure for integer non-linear
-  arithmetic (see Section :ref:`nia <nia>`);
-+ ``lra`` is a decision procedure for linear (real or rational) arithmetic
-  (see Section :ref:`lra <lra>`);
-+ ``nra`` is an incomplete proof procedure for non-linear (real or
-  rational) arithmetic (see Section :ref:`nra <nra>`);
-+ ``psatz D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and
++ :tacn:`lia` is a decision procedure for linear integer arithmetic;
++ :tacn:`nia` is an incomplete proof procedure for integer non-linear
+  arithmetic;
++ :tacn:`lra` is a decision procedure for linear (real or rational) arithmetic;
++ :tacn:`nra` is an incomplete proof procedure for non-linear (real or
+  rational) arithmetic;
++ :tacn:`psatz` ``D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and
   ``n`` is an optional integer limiting the proof search depth
   is an incomplete proof procedure for non-linear arithmetic.
   It is based on John Harrison’s HOL Light
   driver to the external prover `csdp` [#]_. Note that the `csdp` driver is
   generating a *proof cache* which makes it possible to rerun scripts
-  even without `csdp` (see Section :ref:`psatz <psatz>`).
+  even without `csdp`.
 
 The tactics solve propositional formulas parameterized by atomic
 arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}.
@@ -91,12 +90,13 @@ For each conjunct :math:`C_i`, the tactic calls a oracle which searches for
 expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`)
 and checked to be :math:`-1`.
 
-.. _lra:
-
 `lra`: a decision procedure for linear real and rational arithmetic
 -------------------------------------------------------------------
 
-The `lra` tactic is searching for *linear* refutations using Fourier
+.. tacn:: lra
+   :name: lra
+
+This tactic is searching for *linear* refutations using Fourier
 elimination [#]_. As a result, this tactic explores a subset of the *Cone*
 defined as
 
@@ -107,16 +107,17 @@ The deductive power of `lra` is the combined deductive power of
 tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`.
 
 
-.. _lia:
-
 `lia`: a tactic for linear integer arithmetic
 ---------------------------------------------
 
-The tactic lia offers an alternative to the omega and romega tactic
-(see :ref:`omega`). Roughly speaking, the deductive power of lia is
-the combined deductive power of `ring_simplify` and `omega`. However, it
-solves linear goals that `omega` and `romega` do not solve, such as the
-following so-called *omega nightmare* :cite:`TheOmegaPaper`.
+.. tacn:: lia
+   :name: lia
+
+This tactic offers an alternative to the :tacn:`omega` and :tac:`romega`
+tactics. Roughly speaking, the deductive power of lia is the combined deductive
+power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear
+goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following
+so-called *omega nightmare* :cite:`TheOmegaPaper`.
 
 .. coqtop:: in
 
@@ -124,8 +125,8 @@ following so-called *omega nightmare* :cite:`TheOmegaPaper`.
      27 <= 11 * x + 13 * y <= 45 ->
      -10 <= 7 * x - 9 * y <= 4 -> False.
 
-The estimation of the relative efficiency of `lia` *vs* `omega` and `romega`
-is under evaluation.
+The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and
+:tacn:`romega` is under evaluation.
 
 High level view of `lia`
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -182,12 +183,13 @@ Our current oracle tries to find an expression :math:`e` with a small range
 with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for
 a proof.
 
-.. _nra:
-
 `nra`: a proof procedure for non-linear arithmetic
 --------------------------------------------------
 
-The `nra` tactic is an *experimental* proof procedure for non-linear
+.. tacn:: nra
+   :name: nra
+
+This tactic is an *experimental* proof procedure for non-linear
 arithmetic. The tactic performs a limited amount of non-linear
 reasoning before running the linear prover of `lra`. This pre-processing
 does the following:
@@ -202,21 +204,23 @@ does the following:
 After this pre-processing, the linear prover of `lra` searches for a
 proof by abstracting monomials by variables.
 
-.. _nia:
-
 `nia`: a proof procedure for non-linear integer arithmetic
 ----------------------------------------------------------
 
-The `nia` tactic is a proof procedure for non-linear integer arithmetic.
+.. tacn:: nia
+   :name: nia
+
+This tactic is a proof procedure for non-linear integer arithmetic.
 It performs a pre-processing similar to `nra`. The obtained goal is
 solved using the linear integer prover `lia`.
 
-.. _psatz:
-
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
 
-The `psatz` tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the
+.. tacn:: psatz
+   :name: psatz
+
+This tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the
 depth parameter :math:`n`. In theory, such a proof search is complete – if the
 goal is provable the search eventually stops. Unfortunately, the
 external oracle is using numeric (approximate) optimization techniques
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 1c3fdeb43..be30d1bc4 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -151,7 +151,7 @@ Program Definition
    obligations. Once solved using the commands shown below, it binds the
    final |Coq| term to the name ``ident`` in the environment.
 
-   .. exn:: ident already exists
+   .. exn:: @ident already exists (Program Definition)
 
    .. cmdv:: Program Definition @ident : @type := @term
 
@@ -276,6 +276,7 @@ obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
 .. cmd:: {? Local|Global} Obligation Tactic := @tactic
+   :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
    automatically, whether to solve them or when starting to prove one,
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index d6955b310..3e95bd8c4 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -314,28 +314,25 @@ optional priority can be declared, 0 being the highest priority as for
 auto hints. If the priority is not specified, it defaults to the number
 of non-dependent binders of the instance.
 
-Variants:
-
-
-.. cmd:: Instance ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term
+..cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| 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
    singleton classes.
 
-.. cmd:: Global Instance
+..cmdv:: Global Instance
 
    One can use the ``Global`` modifier on instances declared in a
    section so that their generalization is automatically redeclared
    after the section is closed.
 
-.. cmd:: Program Instance
+..cmdv:: Program Instance
 
    Switches the type-checking to Program (chapter :ref:`programs`) and
    uses the obligation mechanism to manage missing fields.
 
-.. cmd:: Declare Instance
+..cmdv:: Declare Instance
 
    In a Module Type, this command states that a corresponding concrete
    instance should exist in any implementation of thisModule Type. This
@@ -370,14 +367,10 @@ Context
 Declares variables according to the given binding context, which might
 use :ref:`implicit-generalization`.
 
+.. tacn:: typeclasses eauto
 
-.. _typeclasses-eauto:
-
-``typeclasses eauto``
-~~~~~~~~~~~~~~~~~~~~~
-
-The ``typeclasses eauto`` tactic uses a different resolution engine than
-eauto and auto. The main differences are the following:
+This tactic uses a different resolution engine than :tacn:`eauto` and
+:tacn:`auto`. The main differences are the following:
 
 + Contrary to ``eauto`` and ``auto``, the resolution is done entirely in
   the new proof engine (as of Coq v8.6), meaning that backtracking is
@@ -428,42 +421,46 @@ Variants:
    typeclass subgoals the same as other subgoals (no shelving of
    non-typeclass goals in particular).
 
-.. _autoapply:
+.. tacn:: autoapply @term with @ident
+   :name: autoapply
 
-``autoapply term with ident``
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The tactic autoapply applies a term using the transparency information
-of the hint database ident, and does *no* typeclass resolution. This can
-be used in ``Hint Extern``’s for typeclass instances (in the hint
-database ``typeclass_instances``) to allow backtracking on the typeclass
-subgoals created by the lemma application, rather than doing type class
-resolution locally at the hint application time.
+   The tactic autoapply applies a term using the transparency information
+   of the hint database ident, and does *no* typeclass resolution. This can
+   be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint
+   database ``typeclass_instances``) to allow backtracking on the typeclass
+   subgoals created by the lemma application, rather than doing type class
+   resolution locally at the hint application time.
 
 .. _TypeclassesTransparent:
 
 Typeclasses Transparent, Typclasses Opaque
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident}
+.. cmd:: Typeclasses Transparent {+ @ident}
 
-   This commands defines the transparency of the given identifiers
-   during type class resolution. It is useful when some constants
-   prevent some unifications and make resolution fail. It is also useful
-   to declare constants which should never be unfolded during
-   proof-search, like fixpoints or anything which does not look like an
-   abbreviation. This can additionally speed up proof search as the
-   typeclass map can be indexed by such rigid constants (see
-   :ref:`thehintsdatabasesforautoandeauto`). By default, all constants
-   and local variables are considered transparent. One should take care
-   not to make opaque any constant that is used to abbreviate a type,
-   like:
+   This command defines makes the identifiers transparent during type class
+   resolution.
 
-::
+   .. cmdv:: Typeclasses Opaque {+ @ident}
+      :name: Typeclasses Opaque
+
+      Make the identifiers opaque for typeclass search. It is useful when some
+      constants prevent some unifications and make resolution fail. It is also
+      useful to declare constants which should never be unfolded during
+      proof-search, like fixpoints or anything which does not look like an
+      abbreviation. This can additionally speed up proof search as the typeclass
+      map can be indexed by such rigid constants (see
+      :ref:`thehintsdatabasesforautoandeauto`).
+
+   By default, all constants and local variables are considered transparent. One
+   should take care not to make opaque any constant that is used to abbreviate a
+   type, like:
+
+   ::
 
-   relation A := A -> A -> Prop.
+      relation A := A -> A -> Prop.
 
-This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
+   This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 
 
 .. opt:: Typeclasses Dependency Order