[refman] Add more missing @ signs

4 files changed, 8 insertions, 7 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/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 92c54e1e1d..0a95a6edd6 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -965,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 b8cbbff2f8..cdd23f4d06 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3305,6 +3305,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This is variant of :n:`unfold @string` where :n:`@string` gets its
    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}}
 
    This is the most general form, where :n:`qualid_or_string` is either a
@@ -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.