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

3 files changed, 27 insertions, 29 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`)
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b0bbbf33b3..82dea1219c 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -131,12 +131,15 @@ class CoqObject(ObjectDescription):
         signature”); for example, the signature of the simplest form of the
         ``exact`` tactic is ``exact @id``.
 
-        Returns None by default, in which case no name will be automatically
-        generated.  This is a convenient way to automatically generate names
-        (link targets) without having to write explicit names everywhere.
+        Generates a name for the directive.  Override this method to return None
+        to avoid generating a name automatically.  This is a convenient way
+        to automatically generate names (link targets) without having to write
+        explicit names everywhere.
 
         """
-        return None
+        m = re.match(r"[a-zA-Z0-9_ ]+", signature)
+        if m:
+            return m.group(0).strip()
 
     def _render_signature(self, signature, signode):
         """Render a signature, placing resulting nodes into signode."""
@@ -343,7 +346,7 @@ class VernacVariantObject(VernacObject):
     def _name_from_signature(self, signature):
         return None
 
-class TacticNotationObject(NotationObject):
+class TacticObject(NotationObject):
     """A tactic, or a tactic notation.
 
     Example::
@@ -356,7 +359,7 @@ class TacticNotationObject(NotationObject):
     index_suffix = "(tactic)"
     annotation = "Tactic"
 
-class AttributeNotationObject(NotationObject):
+class AttributeObject(NotationObject):
     """An attribute.
 
     Example::
@@ -370,7 +373,7 @@ class AttributeNotationObject(NotationObject):
     def _name_from_signature(self, signature):
         return notation_to_string(signature)
 
-class TacticNotationVariantObject(TacticNotationObject):
+class TacticVariantObject(TacticObject):
     """A variant of a tactic.
 
     Example::
@@ -390,6 +393,9 @@ class TacticNotationVariantObject(TacticNotationObject):
     index_suffix = "(tactic variant)"
     annotation = "Variant"
 
+    def _name_from_signature(self, signature):
+        return None
+
 class OptionObject(NotationObject):
     """A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
 
@@ -405,10 +411,6 @@ class OptionObject(NotationObject):
     index_suffix = "(option)"
     annotation = "Option"
 
-    def _name_from_signature(self, signature):
-        return notation_to_string(signature)
-
-
 class FlagObject(NotationObject):
     """A Coq flag (i.e. a boolean setting).
 
@@ -424,10 +426,6 @@ class FlagObject(NotationObject):
     index_suffix = "(flag)"
     annotation = "Flag"
 
-    def _name_from_signature(self, signature):
-        return notation_to_string(signature)
-
-
 class TableObject(NotationObject):
     """A Coq table, i.e. a setting that is a set of values.
 
@@ -442,9 +440,6 @@ class TableObject(NotationObject):
     index_suffix = "(table)"
     annotation = "Table"
 
-    def _name_from_signature(self, signature):
-        return notation_to_string(signature)
-
 class ProductionObject(CoqObject):
     r"""A grammar production.
 
@@ -1251,12 +1246,12 @@ class CoqDomain(Domain):
         # the same role.
         'cmd': VernacObject,
         'cmdv': VernacVariantObject,
-        'tacn': TacticNotationObject,
-        'tacv': TacticNotationVariantObject,
+        'tacn': TacticObject,
+        'tacv': TacticVariantObject,
         'opt': OptionObject,
         'flag': FlagObject,
         'table': TableObject,
-        'attr': AttributeNotationObject,
+        'attr': AttributeObject,
         'thm': GallinaObject,
         'prodn' : ProductionObject,
         'exn': ExceptionObject,