Merge PR #10192: More miscellaneous refman fixes (reopened version of #10187)

Ack-by: Zimmi48

8 files changed, 66 insertions, 61 deletions

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 22ddcae584..45c74ab02a 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -299,9 +299,9 @@ optional tactic is replaced by the default one if not specified.
 
    Displays all remaining obligations.
 
-.. cmd:: Obligation num {? of @ident}
+.. cmd:: Obligation @num {? of @ident}
 
-   Start the proof of obligation num.
+   Start the proof of obligation :token:`num`.
 
 .. cmd:: Next Obligation {? of @ident}
 
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 701c62cdce..db4ebd5e38 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -656,8 +656,8 @@ changes:
     attribute.
 
   - Removed deprecated commands ``Arguments Scope`` and ``Implicit
-    Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper
-    Hugunin.
+    Arguments`` in favor of :cmd:`Arguments (scopes)` and
+    :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin.
 
   - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to
     avoid repeating uniform parameters in constructor declarations.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index c48964d66c..2b673ff62b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1662,6 +1662,7 @@ Declaring Implicit Arguments
    of :token:`qualid`.
 
 .. cmd:: Arguments @qualid : clear implicits
+   :name: Arguments (clear implicits)
 
    This command clears implicit arguments.
 
@@ -1738,6 +1739,7 @@ Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmd:: Arguments @qualid : default implicits
+   :name: Arguments (default implicits)
 
    This command tells |Coq| to automatically detect what are the implicit arguments of a
    defined object.
@@ -1908,6 +1910,7 @@ Renaming implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmd:: Arguments @qualid {* @name} : @rename
+   :name: Arguments (rename)
 
    This command is used to redefine the names of implicit arguments.
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index fed7111628..0a95a6edd6 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -121,6 +121,7 @@ mode but it can also be used in toplevel definitions as shown below.
                      : solve [ `expr` | ... | `expr` ]
                      : idtac [ `message_token` ... `message_token`]
                      : fail [`natural`] [`message_token` ... `message_token`]
+                     : gfail [`natural`] [`message_token` ... `message_token`]
                      : fresh [ `component` … `component` ]
                      : context `ident` [`term`]
                      : eval `redexpr` in `term`
@@ -582,11 +583,11 @@ Failing
       the call to :n:`fail @num` is not enclosed in a :n:`+` command,
       respecting the algebraic identity.
 
-   .. tacv:: fail {* message_token}
+   .. tacv:: fail {* @message_token}
 
       The given tokens are used for printing the failure message.
 
-   .. tacv:: fail @num {* message_token}
+   .. tacv:: fail @num {* @message_token}
 
       This is a combination of the previous variants.
 
@@ -597,8 +598,8 @@ Failing
       Similarly, ``gfail`` fails even when used after ``all:`` and there are no
       goals left. See the example for clarification.
 
-   .. tacv:: gfail {* message_token}
-             gfail @num {* message_token}
+   .. tacv:: gfail {* @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
@@ -964,7 +965,7 @@ system decide a name with the intro tactic is not so good since it is
 very awkward to retrieve the name the system gave. The following
 expression returns an identifier:
 
-.. tacn:: fresh {* component}
+.. tacn:: fresh {* @component}
 
    It evaluates to an identifier unbound in the goal. This fresh identifier
    is obtained by concatenating the value of the :n:`@component`\ s (each of them
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index b19b0742c1..45c40ee787 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1499,7 +1499,7 @@ side of an equation.
 The abstract tactic
 ```````````````````
 
-.. tacn:: abstract: {+ d_item}
+.. tacn:: abstract: {+ @d_item}
    :name: abstract (ssreflect)
 
    This tactic assigns an abstract constant previously introduced with the
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2ee23df019..cdd23f4d06 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2703,33 +2703,33 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
       Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left
 
-   .. tacv:: rewrite @term in clause
+   .. tacv:: rewrite @term in @goal_occurrences
 
       Analogous to :n:`rewrite @term` but rewriting is done following clause
       (similarly to :ref:`performing computations <performingcomputations>`). For instance:
 
-      + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis
-        `H`:sub:`1` instead of the current goal.
-      + :n:`rewrite H in H`:sub:`1` :g:`at 1, H`:sub:`2` :g:`at - 2 |- *` means
-        :n:`rewrite H; rewrite H in H`:sub:`1` :g:`at 1; rewrite H in H`:sub:`2` :g:`at - 2.`
+      + :n:`rewrite H in H'` will rewrite `H` in the hypothesis
+        ``H'`` instead of the current goal.
+      + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means
+        :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.`
         In particular a failure will happen if any of these three simpler tactics
         fails.
-      + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses
-        :g:`H`:sub:`i` different from :g:`H`.
+      + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses
+        :g:`H'` different from :g:`H`.
         A success will happen as soon as at least one of these simpler tactics succeeds.
       + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-`
         that succeeds if at least one of these two tactics succeeds.
 
       Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite.
 
-   .. tacv:: rewrite @term at occurrences
+   .. tacv:: rewrite @term at @occurrences
 
       Rewrite only the given occurrences of :token:`term`. Occurrences are
       specified from left to right as for pattern (:tacn:`pattern`). The rewrite is
       always performed using setoid rewriting, even for Leibniz’s equality, so one
       has to ``Import Setoid`` to use this variant.
 
-   .. tacv:: rewrite @term by tactic
+   .. tacv:: rewrite @term by @tactic
 
       Use tactic to completely solve the side-conditions arising from the
       :tacn:`rewrite`.
@@ -2799,13 +2799,14 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has
       the form :n:`@term’ = @term`
 
-   .. tacv:: replace @term {? with @term} in clause {? by @tactic}
-             replace -> @term in clause
-             replace <- @term in clause
+   .. tacv:: replace @term {? with @term} in @goal_occurences {? by @tactic}
+             replace -> @term in @goal_occurences
+             replace <- @term in @goal_occurences
 
-      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
-      clause argument must not contain any ``type of`` nor ``value of``.
+      Acts as before but the replacements take place in the specified clauses
+      (:token:`goal_occurences`) (see :ref:`performingcomputations`) and not
+      only in the conclusion of the goal. The clause argument must not contain
+      any ``type of`` nor ``value of``.
 
    .. tacv:: cutrewrite <- (@term = @term’)
       :name: cutrewrite
@@ -2893,7 +2894,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
       This applies :n:`stepl @term` then applies :token:`tactic` to the second goal.
 
-   .. tacv:: stepr @term stepr @term by tactic
+   .. tacv:: stepr @term by @tactic
       :name: stepr
 
       This behaves as :tacn:`stepl` but on the right-hand-side of the binary
@@ -3159,7 +3160,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    + A constant can be marked to be unfolded only if applied to enough
      arguments. The number of arguments required can be specified using the
-     ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command.
+     ``/`` symbol in the argument list of the :cmd:`Arguments <Arguments (implicits)>` vernacular command.
 
      .. example::
 
@@ -3299,12 +3300,13 @@ the conversion in hypotheses :n:`{+ @ident}`.
    an expression defining a notation (e.g. `"_ + _"`), and this notation refers to an unfoldable constant, then the
    tactic unfolds it.
 
-.. tacv:: unfold @string%key
+.. tacv:: unfold @string%@ident
 
    This is variant of :n:`unfold @string` where :n:`@string` gets its
-   interpretation from the scope bound to the delimiting key :n:`key`
+   interpretation from the scope bound to the delimiting key :token:`ident`
    instead of its default interpretation (see :ref:`Localinterpretationrulesfornotations`).
-.. tacv:: unfold {+, qualid_or_string at {+, @num}}
+
+.. tacv:: unfold {+, @qualid_or_string at {+, @num}}
 
    This is the most general form, where :n:`qualid_or_string` is either a
    :n:`@qualid` or a :n:`@string` referring to a notation.
@@ -3382,14 +3384,13 @@ the conversion in hypotheses :n:`{+ @ident}`.
 Conversion tactics applied to hypotheses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. tacn:: conv_tactic in {+, @ident}
+.. tacn:: @tactic in {+, @ident}
 
-   Applies the conversion tactic :n:`conv_tactic` to the hypotheses
-   :n:`{+ @ident}`. The tactic :n:`conv_tactic` is any of the conversion tactics
-   listed in this section.
+   Applies :token:`tactic` (any of the conversion tactics listed in this
+   section) to the hypotheses :n:`{+ @ident}`.
 
-   If :n:`@ident` is a local definition, then :n:`@ident` can be replaced by
-   (type of :n:`@ident`) to address not the body but the type of the local
+   If :token:`ident` is a local definition, then :token:`ident` can be replaced by
+   :n:`type of @ident` to address not the body but the type of the local
    definition.
 
    Example: :n:`unfold not in (type of H1) (type of H3)`.
@@ -3550,9 +3551,9 @@ Automation
    This tactic unfolds constants that were declared through a :cmd:`Hint Unfold`
    in the given databases.
 
-.. tacv:: autounfold with {+ @ident} in clause
+.. tacv:: autounfold with {+ @ident} in @goal_occurences
 
-   Performs the unfolding in the given clause.
+   Performs the unfolding in the given clause (:token:`goal_occurences`).
 
 .. tacv:: autounfold with *
 
@@ -3981,7 +3982,7 @@ use one or several databases specific to your development.
    Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in
    the bases :n:`{+ @ident}`.
 
-.. cmd:: Hint Rewrite {+ @term} using tactic : {+ @ident}
+.. cmd:: Hint Rewrite {+ @term} using @tactic : {+ @ident}
 
    When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the
    tactic ``tactic`` will be applied to the generated subgoals, the main subgoal
@@ -4202,7 +4203,7 @@ some incompatibilities.
   Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search
   environment.
 
-.. tacv:: firstorder tactic using {+ @qualid} with {+ @ident}
+.. tacv:: firstorder @tactic using {+ @qualid} with {+ @ident}
 
   This combines the effects of the different variants of :tacn:`firstorder`.
 
@@ -4243,10 +4244,10 @@ some incompatibilities.
       congruence.
       Qed.
 
-.. tacv:: congruence n
+.. tacv:: congruence @num
 
-  Tries to add at most `n` instances of hypotheses stating quantified equalities
-  to the problem in order to solve it. A bigger value of `n` does not make
+  Tries to add at most :token:`num` instances of hypotheses stating quantified equalities
+  to the problem in order to solve it. A bigger value of :token:`num` does not make
   success slower, only failure. You might consider adding some lemmas as
   hypotheses using assert in order for :tacn:`congruence` to use them.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 26dc4e02cf..ffa727ff6c 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -264,11 +264,11 @@ Requests to the environment
       main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or
       `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
 
-   .. cmdv:: Search @string%@key
+   .. cmdv:: Search @string%@ident
 
       The string string must be a notation or the main
       symbol of a notation which is then interpreted in the scope bound to
-      the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`).
+      the delimiting key :token:`ident` (see Section :ref:`LocalInterpretationRulesForNotations`).
 
    .. cmdv:: Search @term_pattern
 
@@ -1208,7 +1208,7 @@ Controlling the locality of commands
      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
+     the :cmd:`Arguments <Arguments (implicits)>`, :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.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6da42f4a48..3710c0af9d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1032,11 +1032,11 @@ Local opening of an interpretation scope
 +++++++++++++++++++++++++++++++++++++++++
 
 It is possible to locally extend the interpretation scope stack using the syntax
-:g:`(term)%key` (or simply :g:`term%key` for atomic terms), where key is a
+:n:`(@term)%@ident` (or simply :n:`@term%@ident` for atomic terms), where :token:`ident` is a
 special identifier called *delimiting key* and bound to a given scope.
 
 In such a situation, the term term, and all its subterms, are
-interpreted in the scope stack extended with the scope bound tokey.
+interpreted in the scope stack extended with the scope bound to :token:`ident`.
 
 .. cmd:: Delimit Scope @scope with @ident
 
@@ -1051,15 +1051,15 @@ interpreted in the scope stack extended with the scope bound tokey.
 Binding arguments of a constant to an interpretation scope
 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
-.. cmd:: Arguments @qualid {+ @name%@scope}
+.. cmd:: Arguments @qualid {+ @name%@ident}
    :name: Arguments (scopes)
 
    It is possible to set in advance that some arguments of a given constant have
    to be interpreted in a given scope. The command is
-   :n:`Arguments @qualid {+ @name%@scope}` where the list is a prefix of the
-   arguments of ``qualid`` eventually annotated with their ``scope``. Grouping
+   :n:`Arguments @qualid {+ @name%@ident}` where the list is a prefix of the
+   arguments of ``qualid`` optionally annotated with their scope :token:`ident`. Grouping
    round parentheses can be used to decorate multiple arguments with the same
-   scope. ``scope`` can be either a scope name or its delimiting key. For
+   scope. :token:`ident` can be either a scope name or its delimiting key. For
    example the following command puts the first two arguments of :g:`plus_fct`
    in the scope delimited by the key ``F`` (``Rfun_scope``) and the last
    argument in the scope delimited by the key ``R`` (``R_scope``).
@@ -1070,13 +1070,13 @@ Binding arguments of a constant to an interpretation scope
 
    The ``Arguments`` command accepts scopes decoration to all grouping
    parentheses. In the following example arguments A and B are marked as
-   maximally inserted implicit arguments and are put into the type_scope scope.
+   maximally inserted implicit arguments and are put into the ``type_scope`` scope.
 
    .. coqdoc::
 
       Arguments respectful {A B}%type (R R')%signature _ _.
 
-   When interpreting a term, if some of the arguments of qualid are built
+   When interpreting a term, if some of the arguments of :token:`qualid` are built
    from a notation, then this notation is interpreted in the scope stack
    extended by the scope bound (if any) to this argument. The effect of
    the scope is limited to the argument itself. It does not propagate to
@@ -1088,21 +1088,21 @@ Binding arguments of a constant to an interpretation scope
 
       This command can be used to clear argument scopes of :token:`qualid`.
 
-   .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes
+   .. cmdv:: Arguments @qualid {+ @name%@ident} : extra scopes
 
       Defines extra argument scopes, to be used in case of coercion to ``Funclass``
       (see the :ref:`implicitcoercions` chapter) or with a computed type.
 
-   .. cmdv:: Global Arguments @qualid {+ @name%@scope}
+   .. cmdv:: Global Arguments @qualid {+ @name%@ident}
 
-      This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a
+      This behaves like :n:`Arguments qualid {+ @name%@ident}` but survives when a
       section is closed instead of stopping working at section closing. Without the
       ``Global`` modifier, the effect of the command stops when the section it belongs
       to ends.
 
-   .. cmdv:: Local Arguments @qualid {+ @name%@scope}
+   .. cmdv:: Local Arguments @qualid {+ @name%@ident}
 
-      This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not
+      This behaves like :n:`Arguments @qualid {+ @name%@ident}` but does not
       survive modules and files. Without the ``Local`` modifier, the effect of the
       command is visible from within other modules or files.
 
@@ -1143,8 +1143,8 @@ Binding types of arguments to an interpretation scope
    scope of operations on the natural numbers), it may be convenient to bind it
    to this type. When a scope ``scope`` is bound to a type ``type``, any new function
    defined later on gets its arguments of type ``type`` interpreted by default in
-   scope scope (this default behavior can however be overwritten by explicitly
-   using the command :cmd:`Arguments`).
+   scope ``scope`` (this default behavior can however be overwritten by explicitly
+   using the command :cmd:`Arguments <Arguments (scopes)>`).
 
    Whether the argument of a function has some type ``type`` is determined
    statically. For instance, if ``f`` is a polymorphic function of type