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

2 files changed, 11 insertions, 8 deletions

diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 2a321b5cbf..f037fed394 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -102,7 +102,7 @@ forget this paragraph and use the tactic according to your intuition.
 Concrete usage in Coq
 --------------------------
 
-.. tacn:: ring
+.. tacv:: ring
 
    This tactic solves equations upon polynomial expressions of a ring
    (or semiring) structure. It proceeds by normalizing both sides
@@ -110,7 +110,7 @@ Concrete usage in Coq
    distributivity, constant propagation, rewriting of monomials) and
    comparing syntactically the results.
 
-.. tacn:: ring_simplify
+.. tacv:: ring_simplify
 
    This tactic applies the normalization procedure described above to
    the given terms. The tactic then replaces all occurrences of the terms
@@ -511,7 +511,7 @@ application of the main correctness theorem to well-chosen arguments.
 Dealing with fields
 ------------------------
 
-.. tacn:: field
+.. tacv:: field
 
    This tactic is an extension of the :tacn:`ring` tactic that deals with rational
    expressions. Given a rational expression :math:`F = 0`. It first reduces the
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`)