1 files changed, 15 insertions, 6 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6ddb0b027..977a5b8fa 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -493,7 +493,10 @@ inferred from the whole context of the goal (see for example section
 Definitions
 ~~~~~~~~~~~
 
-The pose tactic allows to add a defined constant to a proof context.
+.. tacn:: pose
+   :name: pose (ssreflect)
+
+This tactic allows to add a defined constant to a proof context.
 |SSR| generalizes this tactic in several ways. In particular, the
 |SSR| pose tactic supports *open syntax*: the body of the
 definition does not need surrounding parentheses. For instance:
@@ -1349,6 +1352,7 @@ Discharge
 The general syntax of the discharging tactical ``:`` is:
 
 .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch }
+   :name: ... : ... (ssreflect)
 
 .. prodn::
    d_item ::= {? @occ_switch %| @clear_switch } @term
@@ -1500,9 +1504,11 @@ side of an equation.
 The abstract tactic
 ```````````````````
 
-The ``abstract`` tactic assigns an ``abstract`` constant previously
-introduced with the ``[: name ]`` intro pattern
-(see section :ref:`introduction_ssr`).
+.. tacn:: abstract: {+ d_item}
+   :name abstract (ssreflect)
+
+This tactic assigns an abstract constant previously introduced with the ``[:
+name ]`` intro pattern (see section :ref:`introduction_ssr`).
 
 In a goal like the following::
 
@@ -1809,6 +1815,8 @@ of a :token:`d_item` immediately following this ``/`` switch,
 using the syntax:
 
 .. tacv:: case: {+ @d_item } / {+ @d_item }
+   :name: case (ssreflect)
+
 .. tacv:: elim: {+ @d_item } / {+ @d_item }
 
 The :token:`d_item` on the right side of the ``/`` switch are discharged as
@@ -2132,7 +2140,7 @@ tactic using the given second tactic, and fails if it does not succeed.
 Its analogue
 
 .. tacn:: @tactic ; first by @tactic
-   :name: first
+   :name: first (ssreflect)
 
 tries to solve the first subgoal generated by the first tactic using the
 second given tactic, and fails if it does not succeed.
@@ -2212,7 +2220,7 @@ Iteration
 thanks to the do tactical, whose general syntax is:
 
 .. tacn:: do {? @mult } ( @tactic | [ {+| @tactic } ] )
-   :name: do
+   :name: do (ssreflect)
 
 where :token:`mult` is a *multiplier*.
 
@@ -3724,6 +3732,7 @@ We provide a special tactic unlock for unfolding such definitions
 while removing “locks”, e.g., the tactic:
 
 .. tacn:: unlock {? @occ_switch } @ident
+   :name: unlock
 
 replaces the occurrence(s) of :token:`ident` coded by the
 :token:`occ_switch` with the corresponding body.