Merge PR #7374: [sphinx] More fatal warnings.

10 files changed, 106 insertions, 77 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index f5237e4fb..e10e16c10 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -599,6 +599,7 @@ Notice that the syntax is not completely backward compatible since the
 identifier was not required.
 
 .. cmd:: Add Morphism f : @ident
+   :name: Add Morphism
 
 The latter command also is restricted to the declaration of morphisms
 without parameters. It is not fully backward compatible since the
@@ -616,7 +617,7 @@ the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can
 used to replace terms in contexts that were refused by the old
 implementation. As discussed in the next section, the semantics of the
 new :tacn:`setoid_rewrite` tactic differs slightly from the old one and
-tacn:`rewrite`.
+:tacn:`rewrite`.
 
 
 Extensions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 5f8c06484..152f4f655 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -263,9 +263,12 @@ Activating the Printing of Coercions
 
 .. cmd:: Add Printing Coercion @qualid
 
-  This command forces coercion denoted by :n:`@qualid` to be printed. To skip
-  the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By
-  default, a coercion is never printed.
+   This command forces coercion denoted by :n:`@qualid` to be printed.
+   By default, a coercion is never printed.
+
+.. cmd:: Remove Printing Coercion @qualid
+
+   Use this command, to skip the printing of coercion :n:`@qualid`.
 
 .. _coercions-classes-as-records:
 
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 009efd0d2..80ce01620 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -26,6 +26,11 @@ solvable. This is the restriction meant by "Presburger arithmetic".
 If the tactic cannot solve the goal, it fails with an error message.
 In any case, the computation eventually stops.
 
+.. tacv:: romega
+   :name: romega
+
+   To be documented.
+
 Arithmetical goals recognized by ``omega``
 ------------------------------------------
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8746897e7..53b993edd 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1175,52 +1175,53 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
     If `qualid` denotes a valid basic module (i.e. its module type is a
     signature), makes its components available by their short names.
 
-.. example::
+    .. example::
 
-    .. coqtop:: reset all
+       .. coqtop:: reset all
 
-       Module Mod.
+          Module Mod.
 
-       Definition T:=nat.
+          Definition T:=nat.
 
-       Check T.
+          Check T.
 
-       End Mod.
+          End Mod.
 
-       Check Mod.T.
+          Check Mod.T.
 
-       Fail Check T.
+          Fail Check T.
 
-       Import Mod.
+          Import Mod.
 
-       Check T.
+          Check T.
 
-Some features defined in modules are activated only when a module is
-imported. This is for instance the case of notations (see :ref:`Notations`).
+    Some features defined in modules are activated only when a module is
+    imported. This is for instance the case of notations (see :ref:`Notations`).
 
-Declarations made with the Local flag are never imported by theImport
-command. Such declarations are only accessible through their fully
-qualified name.
+    Declarations made with the ``Local`` flag are never imported by the :cmd:`Import`
+    command. Such declarations are only accessible through their fully
+    qualified name.
 
-.. example::
+    .. example::
 
-    .. coqtop:: all
+       .. coqtop:: all
 
-       Module A.
+          Module A.
 
-       Module B.
+          Module B.
 
-       Local Definition T := nat.
+          Local Definition T := nat.
 
-       End B.
+          End B.
 
-       End A.
+          End A.
 
-       Import A.
+          Import A.
 
-       Fail Check B.T.
+          Fail Check B.T.
 
     .. cmdv:: Export @qualid
+       :name: Export
 
        When the module containing the command Export qualid
        is imported, qualid is imported as well.
@@ -1231,16 +1232,17 @@ qualified name.
 
 .. cmd:: Print Module @ident
 
-    Prints the module type and (optionally) the body of the module `ident`.
+   Prints the module type and (optionally) the body of the module :n:`@ident`.
 
 .. cmd:: Print Module Type @ident
 
-    Prints the module type corresponding to `ident`.
+   Prints the module type corresponding to :n:`@ident`.
 
 .. opt:: Short Module Printing
 
-    This option (off by default) disables the printing of the types of fields,
-    leaving only their names, for the commands ``Print Module`` and ``Print Module Type``.
+   This option (off by default) disables the printing of the types of fields,
+   leaving only their names, for the commands :cmd:`Print Module` and
+   :cmd:`Print Module Type`.
 
 Libraries and qualified names
 ---------------------------------
@@ -1510,9 +1512,8 @@ implicitly applied to the implicit arguments it is waiting for: one
 says that the implicit argument is maximally inserted.
 
 Each implicit argument can be declared to have to be inserted maximally or non
-maximally. This can be governed argument per argument by the command ``Implicit
-Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the
-:opt:`Maximal Implicit Insertion` option.
+maximally. This can be governed argument per argument by the command
+:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option.
 See also :ref:`displaying-implicit-args`.
 
 
@@ -1565,7 +1566,7 @@ absent in every situation but still be able to specify it if needed:
 
 
 The syntax is supported in all top-level definitions:
-``Definition``, ``Fixpoint``, ``Lemma`` and so on. For (co-)inductive datatype
+:cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype
 declarations, the semantics are the following: an inductive parameter
 declared as an implicit argument need not be repeated in the inductive
 definition but will become implicit for the constructors of the
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 46e684b12..39735a6ed 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -609,6 +609,7 @@ of any section is equivalent to using ``Local Parameter``.
    Adds blocks of variables with different specifications.
 
 .. cmdv:: Variables {+ ( {+ @ident } : @term) }
+   :name: Variables
 
 .. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }
    :name: Hypothesis
@@ -672,6 +673,7 @@ Section :ref:`typing-rules`.
    You have to explicitly give their fully qualified name to refer to them.
 
 .. cmdv:: Example @ident := @term
+   :name: Example
 
 .. cmdv:: Example @ident : @term := @term
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c5ee724ca..2b128b98f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -245,7 +245,7 @@ focused goals with:
    :name: ... : ... (goal selector)
 
    We can also use selectors as a tactical, which allows to use them nested
-   in a tactic expression, by using the keyword :tacn:`only`:
+   in a tactic expression, by using the keyword ``only``:
 
    .. tacv:: only selector : expr
       :name: only ... : ...
@@ -826,6 +826,7 @@ We can make pattern matching on goals using the following expression:
 .. we should provide the full grammar here
 
 .. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+   :name: match goal
 
    If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is
    matched (non-linear first-order unification) by an hypothesis of the
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 20a362c4c..0318bddde 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -648,6 +648,7 @@ be applied or the goal is not head-reducible.
 .. exn:: @ident is already used.
 
 .. tacv:: intros
+   :name: intros
 
    This repeats ``intro`` until it meets the head-constant. It never
    reduces head-constants and it never fails.
@@ -714,7 +715,7 @@ be applied or the goal is not head-reducible.
 
    These tactics behave as previously but naming the introduced hypothesis
    :n:`@ident`. It is equivalent to :n:`intro @ident` followed by the
-   appropriate call to move (see :tacn:`move ... after`).
+   appropriate call to ``move`` (see :tacn:`move ... after ...`).
 
 .. tacn:: intros @intro_pattern_list
    :name: intros ...
@@ -917,7 +918,7 @@ the inverse of :tacn:`intro`.
    depend on it.
 
 .. tacn:: move @ident after @ident
-   :name: move .. after ...
+   :name: move ... after ...
 
    This moves the hypothesis named :n:`@ident` in the local context after the
    hypothesis named :n:`@ident`, where “after” is in reference to the
@@ -2148,7 +2149,7 @@ See also: :ref:`advanced-recursive-functions`
    :n:`dependent inversion_clear @ident`.
 
 .. tacv:: dependent inversion @ident with @term
-   :name: dependent inversion ...
+   :name: dependent inversion ... with ...
 
    This variant allows you to specify the generalization of the goal. It is
    useful when the system fails to generalize the goal automatically. If
@@ -2163,7 +2164,7 @@ See also: :ref:`advanced-recursive-functions`
 
 .. tacv:: dependent inversion_clear @ident with @term
 
-   Like :tacn:`dependent inversion ...` with but clears :n:`@ident` from the
+   Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the
    local context.
 
 .. tacv:: dependent inversion_clear @ident as @intro_pattern with @term
@@ -3193,7 +3194,7 @@ can solve such a goal:
       Goal forall P:nat -> Prop, P 0 -> exists n, P n.
       eauto.
 
-Note that :tacn:`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}}
@@ -3444,6 +3445,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       Declares each :n:`@ident` as a transparent or opaque constant.
 
    .. cmdv:: Hint Extern @num {? @pattern} => tactic
+      :name: Hint Extern
 
       This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
       :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
@@ -3664,6 +3666,7 @@ option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.
 
 .. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %)
+   :name: Loose Hint Behavior
 
    This option accepts three values, which control the behavior of hints w.r.t.
    :cmd:`Import`:
@@ -3808,14 +3811,15 @@ some incompatibilities.
 
 .. tacv:: intuition
 
-  Is equivalent to :g:`intuition auto with *`.
+   Is equivalent to :g:`intuition auto with *`.
 
 .. tacv:: dintuition
+   :name: dintuition
 
-  While :tacn:`intuition` recognizes inductively defined connectives
-  isomorphic to the standard connective ``and, prod, or, sum, False,
-  Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive
-  types with one constructors and no indices, i.e. record-style connectives.
+   While :tacn:`intuition` recognizes inductively defined connectives
+   isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``,
+   ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive
+   types with one constructors and no indices, i.e. record-style connectives.
 
 .. opt:: Intuition Negation Unfolding
 
@@ -3844,11 +3848,14 @@ 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
+.. opt:: Firstorder Solver @tactic
 
    The default tactic used by :tacn:`firstorder` when no rule applies is
-   :g:`auto with *`, it can be reset locally or globally using this option and
-   printed using :cmd:`Print Firstorder Solver`.
+   :g:`auto with *`, it can be reset locally or globally using this option.
+
+   .. cmd:: Print Firstorder Solver
+
+      Prints the default tactic used by :tacn:`firstorder` when no rule applies.
 
 .. tacv:: firstorder @tactic
 
@@ -4011,8 +4018,8 @@ solved by :tacn:`f_equal`.
    :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
-:tacn:`refl_equal`.
+and `u` are convertible and then solves the goal. It is equivalent to
+``apply refl_equal``.
 
 .. exn:: The conclusion is not a substitutive equation.
 
@@ -4104,7 +4111,7 @@ symbol :g:`=`.
    :n:`intro @ident; simplify_eq @ident`.
 
 .. tacn:: dependent rewrite -> @ident
-   :name: dependent rewrite
+   :name: dependent rewrite ->
 
    This tactic applies to any goal. If :n:`@ident` has type
    :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each
@@ -4115,6 +4122,7 @@ symbol :g:`=`.
    :tacn:`injection` and :tacn:`inversion` tactics.
 
 .. tacv:: dependent rewrite <- @ident
+   :name: dependent rewrite <-
 
    Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to
    left.
@@ -4374,19 +4382,20 @@ This tactics reverses the list of the focused goals.
    unification, or they can be called back into focus with the command
    :cmd:`Unshelve`.
 
-.. tacv:: shelve_unifiable
+   .. tacv:: shelve_unifiable
+      :name: shelve_unifiable
 
-   Shelves only the goals under focus that are mentioned in other goals.
-   Goals that appear in the type of other goals can be solved by unification.
+      Shelves only the goals under focus that are mentioned in other goals.
+      Goals that appear in the type of other goals can be solved by unification.
 
-.. example::
+      .. example::
 
-   .. coqtop:: all reset
+         .. coqtop:: all reset
 
-      Goal exists n, n=0.
-      refine (ex_intro _ _ _).
-      all:shelve_unifiable.
-      reflexivity.
+            Goal exists n, n=0.
+            refine (ex_intro _ _ _).
+            all: shelve_unifiable.
+            reflexivity.
 
 .. cmd:: Unshelve
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7ba103b22..c37233734 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -360,6 +360,7 @@ Requests to the environment
             Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
    .. cmdv:: SearchAbout
+      :name: SearchAbout
 
       .. deprecated:: 8.5
 
@@ -416,7 +417,7 @@ Requests to the environment
    current goal (if any) and theorems of the current context whose
    statement’s conclusion or last hypothesis and conclusion matches the
    expressionterm where holes in the latter are denoted by `_`.
-   It is a variant of Search @term_pattern that does not look for subterms
+   It is a variant of :n:`Search @term_pattern` that does not look for subterms
    but searches for statements whose conclusion has exactly the expected
    form, or whose statement finishes by the given series of
    hypothesis/conclusion.
@@ -625,6 +626,7 @@ file is a particular case of module called *library file*.
 
 
    .. cmdv:: Require Import @qualid
+      :name: Require Import
 
       This loads and declares the module :n:`@qualid`
       and its dependencies then imports the contents of :n:`@qualid` as described
@@ -637,10 +639,11 @@ file is a particular case of module called *library file*.
       :cmd:`Import` :n:`@qualid` would.
 
    .. cmdv:: Require Export @qualid
+      :name: Require Export
 
-      This command acts as ``Require Import`` :n:`@qualid`,
-      but if a further module, say `A`, contains a command ``Require Export`` `B`,
-      then the command ``Require Import`` `A` also imports the module `B.`
+      This command acts as :cmd:`Require Import` :n:`@qualid`,
+      but if a further module, say `A`, contains a command :cmd:`Require Export` `B`,
+      then the command :cmd:`Require Import` `A` also imports the module `B.`
 
    .. cmdv:: Require [Import | Export] {+ @qualid }
 
@@ -653,7 +656,7 @@ file is a particular case of module called *library file*.
 
    .. cmdv:: From @dirpath Require @qualid
 
-      This command acts as ``Require``, but picks
+      This command acts as :cmd:`Require`, but picks
       any library whose absolute name is of the form dirpath.dirpath’.qualid
       for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library
       comes from a given package by making explicit its absolute root.
@@ -895,6 +898,7 @@ interactively, they cannot be part of a vernacular file loaded via
    necessary.
 
    .. cmdv:: Backtrack @num @num @num
+      :name: Backtrack
 
       .. deprecated:: 8.4
 
@@ -1022,12 +1026,14 @@ Controlling display
    output, printing only identifiers.
 
 .. opt:: Printing Width @num
+   :name: Printing Width
 
    This command sets which left-aligned part of the width of the screen is used
    for display. At the time of writing this documentation, the default value
    is 78.
 
 .. opt:: Printing Depth @num
+   :name: Printing Depth
 
    This option controls the nesting depth of the formatter used for pretty-
    printing. Beyond this depth, display of subterms is replaced by dots. At the
@@ -1208,28 +1214,29 @@ 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 ``Coercion``
-  (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-strategy>`)
-  commands belong to this category.
+  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 extent 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:`Implicit Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
+  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 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
+  of the section or module they occur in.  For these commands, the ``Global``
   modifier extends their effect outside the sections and modules they
-  occurs in.  The ``Transparent`` and ``Opaque`` (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands  belong to this category.
+  occurs 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 ``Set`` and ``Unset`` commands belong to this
+  occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
   category.
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index e12e4d897..682553c31 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -26,6 +26,7 @@ induction for objects in type `identᵢ`.
   natural in case of inductively defined relations.
 
 .. cmdv:: Scheme Equality for @ident
+   :name: Scheme Equality
 
    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.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6958b5f26..3b95a37ed 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -916,9 +916,8 @@ Binding arguments of a constant to an interpretation scope
 
 .. seealso::
 
-   :cmd:`About @qualid`
-     The command to show the scopes bound to the arguments of a
-     function is described in Section 2.
+   The command :cmd:`About` can be used to show the scopes bound to the
+   arguments of a function.
 
 .. note::