Make automatic name generation for directives more consistent:

- by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except
- don't generate a name for cmdv and tacv
- generate more flexibily for exn, warn and attr

1 files changed, 8 insertions, 5 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index f8435fcffe..9ee61a801a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2232,6 +2232,7 @@ tactics to *permute* the subgoals generated by a tactic.
       circular order of subgoals remains unchanged.
 
    .. tacn:: first @num last
+      :name: first (ssreflect)
 
       If :token:`num`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
@@ -5653,22 +5654,23 @@ respectively.
 
 .. tacn:: apply
           exact
+   :name: apply (ssreflect); exact (ssreflect)
 
    application (see :ref:`the_defective_tactics_ssr`)
 
-.. tacn:: abstract
+.. tacv:: abstract
 
    see :ref:`abstract_ssr` and :ref:`generating_let_ssr`
 
-.. tacn:: elim
+.. tacv:: elim
 
    induction (see :ref:`the_defective_tactics_ssr`)
 
-.. tacn:: case
+.. tacv:: case
 
    case analysis (see :ref:`the_defective_tactics_ssr`)
 
-.. tacn:: rewrite {+ @r_step }
+.. tacv:: rewrite {+ @r_step }
 
    rewrite (see :ref:`rewriting_ssr`)
 
@@ -5702,7 +5704,7 @@ respectively.
 
    backchaining (see :ref:`structure_ssr`)
 
-.. tacn:: pose @ident := @term
+.. tacv:: pose @ident := @term
 
    local definition (see :ref:`definitions_ssr`)
 
@@ -5719,6 +5721,7 @@ respectively.
    local cofix definition
 
 .. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) }
+   :name: set (ssreflect)
 
    abbreviation (see :ref:`abbreviations_ssr`)