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

3 files changed, 55 insertions, 38 deletions

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.