[refman] Misc fixes (mostly missing '@' signs)

Co-Authored-By: @Zimmi48

4 files changed, 49 insertions, 48 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index fed7111628..92c54e1e1d 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
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index cd023eb1b1..b8cbbff2f8 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
@@ -3299,12 +3300,12 @@ 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 +3383,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 +3550,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 +3981,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 +4202,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`.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index fa5ca81a7c..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
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6a681d83f0..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.