Support multiple :name:s with multiple signatures for .. tacn::

doc/sphinx/addendum/generalized-rewriting.rst

@@ -576,7 +576,6 @@ pass additional arguments such as ``using relation``.
           setoid_rewrite {? {| -> | <- } } @one_term_with_bindings {? at @rewrite_occs } {? in @ident }
           setoid_rewrite {? {| -> | <- } } @one_term_with_bindings in @ident at @rewrite_occs
           setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 }
-   :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_etransitivity; setoid_rewrite; _; setoid_replace
 
    .. todo: move rewrite_occs to rewrite chapter when that chapter is revised
 
@@ -638,7 +637,6 @@ Deprecated syntax and backward incompatibilities
 
 .. cmd:: Add Morphism @one_term : @ident
          Add Morphism @one_term with signature @term as @ident
-   :name: Add Morphism; _
 
    This command is restricted to the declaration of morphisms
    without parameters. It is not fully backward compatible since the
@@ -776,7 +774,6 @@ Usage
 ~~~~~
 
 .. tacn:: rewrite_strat @rewstrategy {? in @ident }
-   :name: rewrite_strat
 
    Rewrite using :n:`@rewstrategy` in the conclusion or in the hypothesis :n:`@ident`.
 

doc/sphinx/language/core/assumptions.rst

@@ -198,7 +198,7 @@ has type :n:`@type`.
        Axiom R_S_inv : forall x y, R x y <-> S y x.
 
 .. exn:: @ident already exists.
-   :name: ‘ident’ already exists. (Axiom)
+   :name: ‘ident’ already exists (Axiom)
    :undocumented:
 
 .. warn:: @ident is declared as a local axiom

doc/sphinx/language/core/definitions.rst

@@ -115,7 +115,7 @@ Section :ref:`typing-rules`.
    .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
    .. exn:: @ident already exists.
-      :name: ‘ident’ already exists. (Definition)
+      :name: ‘ident’ already exists (Definition)
       :undocumented:
 
    .. exn:: The term @term has type @type while it is expected to have type @type'.
@@ -177,7 +177,7 @@ The basic assertion command is:
       :undocumented:
 
    .. exn:: @ident already exists.
-      :name: ‘ident’ already exists. (Theorem)
+      :name: ‘ident’ already exists (Theorem)
 
       The name you provided is already defined. You have then to choose
       another name.

doc/sphinx/language/core/records.rst

@@ -185,6 +185,7 @@ Defining record types
       :cmd:`CoInductive` command instead.
 
    .. exn:: @ident already exists
+      :name: ‘ident’ already exists (Record)
 
       The fieldname :n:`@ident` is already defined as a global.
 

doc/sphinx/language/core/sections.rst

@@ -52,7 +52,6 @@ usable outside the section as shown in this :ref:`example <section_local_declara
 .. cmd:: Let @ident_decl @def_body
          Let Fixpoint @fix_definition {* with @fix_definition }
          Let CoFixpoint @cofix_definition {* with @cofix_definition }
-   :name: Let; Let Fixpoint; Let CoFixpoint
 
    These are similar to :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that
    the declared :term:`constant` is local to the current section.

doc/sphinx/proof-engine/tactics.rst

@@ -1381,7 +1381,6 @@ Managing the local context
 
 .. tacn:: set @alias_definition {? @occurrences }
           set @one_term {? @as_name } {? @occurrences }
-   :name: set; _
 
    .. insertprodn alias_definition as_name
 
@@ -1428,7 +1427,6 @@ Managing the local context
 
    .. tacn:: eset @alias_definition {? @occurrences }
              eset @one_term {? @as_name } {? @occurrences }
-      :name: eset; _
 
       Similar to :tacn:`set`, but instead of failing because of uninstantiated
       variables, generates existential variables for them.
@@ -1452,14 +1450,12 @@ Managing the local context
 
 .. tacn:: pose @alias_definition
           pose @one_term {? @as_name }
-   :name: pose; _
 
    Similar to :tacn:`set`.  Adds a :term:`local definition <context-local definition>`
    to the context but without doing any replacement.
 
    .. tacn:: epose @alias_definition
              epose @one_term {? @as_name }
-      :name: epose; _
 
       Similar to :tacn:`pose`, but instead of failing because of uninstantiated
       variables, generates existential variables for them.
@@ -1481,7 +1477,6 @@ Controlling the proof flow
 .. tacn:: assert ( @ident : @type ) {? by @ltac_expr3 }
           assert ( @ident := @term )
           assert @one_type {? @as_ipat } {? by @ltac_expr3 }
-   :name: assert; _; _
 
    Adds a new hypothesis to the current subgoal and a new subgoal before
    it to prove the hypothesis.  Then, if :n:`@ltac_expr3`
@@ -1514,7 +1509,6 @@ Controlling the proof flow
    .. tacn:: eassert ( @ident : @type ) {? by @ltac_expr3 }
              eassert ( @ident := @term )
              eassert @one_type {? @as_ipat } {? by @ltac_expr3 }
-      :name: eassert; _; _
 
       Unlike :tacn:`assert`, the :n:`@type`, :n:`@term` or :n:`@one_type` in
       :tacn:`eassert` may contain :gdef:`holes <hole>`, denoted by :n:`_`,
@@ -1524,7 +1518,6 @@ Controlling the proof flow
 
 .. tacn:: enough ( @ident : @type ) {? by @ltac_expr3 }
           enough @one_type {? @as_ipat } {? by @ltac_expr3 }
-   :name: enough; _
 
    Adds a new hypothesis to the current subgoal and a new subgoal after it
    to prove the hypothesis.
@@ -1543,7 +1536,6 @@ Controlling the proof flow
 
    .. tacn:: eenough ( @ident : @type ) {? by @ltac_expr3 }
              eenough @one_type {? @as_ipat } {? by @ltac_expr3 }
-      :name: eenough; _
 
       Unlike :tacn:`enough`, the :n:`@type` and :n:`@one_type` in
       :tacn:`eenough` may contain :term:`holes <hole>`, denoted by :n:`_`,
@@ -1561,7 +1553,6 @@ Controlling the proof flow
 
 .. tacn:: pose proof @term {? @as_ipat }
           pose proof ( @ident := @term )
-   :name: pose proof; _
 
    The first form behaves like :n:`assert @one_type {? @as_ipat } by exact @term`
    where :token:`one_type` is the type of :token:`term`.
@@ -1572,7 +1563,6 @@ Controlling the proof flow
 
    .. tacn:: epose proof @term {? @as_ipat }
              epose proof ( @ident := @term )
-      :name: epose proof; _
 
       While :tacn:`pose proof` expects that no existential variables are generated by
       the tactic, :tacn:`epose proof` removes this constraint.
@@ -1651,7 +1641,6 @@ Controlling the proof flow
 
 .. tacn:: generalize {+ @one_term }
           generalize {+, @pattern_occs {? @as_name } }
-   :name: generalize; _
 
    For each :n:`@one_term` (which may be in the :n:`@pattern_occs`), replaces the
    goal `G` with `forall (x:T), G'`,
@@ -1698,7 +1687,6 @@ Controlling the proof flow
 
 .. tacn:: evar ( @ident : @type )
           evar @one_type
-   :name: evar; _
 
    The :n:`evar` tactic creates a new :term:`local definition <context-local definition>`
    named :n:`@ident` with type :n:`@type` or :n:`@one_type` in the context.
@@ -1707,7 +1695,6 @@ Controlling the proof flow
 
 .. tacn:: instantiate ( @ident := @term )
           instantiate ( @natural := @term ) {? @hloc }
-   :name: instantiate; _
 
    .. insertprodn hloc hloc
 

doc/sphinx/proofs/automatic-tactics/auto.rst

@@ -379,7 +379,6 @@ Creating Hints
 
    .. cmd:: Hint Resolve {+ {| @qualid | @one_term } } {? @hint_info } {? : {+ @ident } }
             Hint Resolve {| -> | <- } {+ @qualid } {? @natural } {? : {+ @ident } }
-      :name: Hint Resolve; _
 
       .. insertprodn hint_info one_pattern
 

doc/sphinx/proofs/writing-proofs/equality.rst

@@ -240,7 +240,6 @@ Rewriting with Leibniz and setoid equality
 
 .. tacn:: replace @one_term__from with @one_term__to {? @occurrences } {? by @ltac_expr3 }
           replace {? {| -> | <- } } @one_term__from {? @occurrences }
-   :name: replace; _
 
    The first form replaces all free occurrences of :n:`@one_term__from`
    in the current goal with :n:`@one_term__to` and generates an equality

doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst

@@ -733,7 +733,6 @@ This section describes some special purpose tactics to work with
 
 .. tacn:: inversion {| @ident | @natural } {? as @or_and_intropattern } {? in {+ @ident } }
           inversion {| @ident | @natural } using @one_term {? in {+ @ident } }
-   :name: inversion; _
 
    .. comment: the other inversion* tactics don't support the using clause,
       but they should be able to, if desired.  It wouldn't make sense for

doc/tools/coqrst/coqdomain.py

@@ -159,7 +159,7 @@ def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused
         explicit names everywhere.
 
         """
-        m = re.match(r"[a-zA-Z0-9_ ]+", signature)
+        m = re.match(r"[a-zA-Z0-9_ \(\)]+", signature)
         if m:
             return m.group(0).strip()
 
@@ -274,14 +274,12 @@ def _prepare_names(self):
             self._sig_names = {}
         else:
             names = [n.strip() for n in names.split(";")]
-            if len(names) != len(sigs):
-                if len(sigs) != 1: #Multiple names for one signature
-                    ERR = ("Expected {} semicolon-separated names, got {}.  " +
-                           "Please provide one name per signature line.")
-                    raise self.error(ERR.format(len(names), len(sigs)))
-                self._sig_names = { sigs[0]: names }
-            else:
-                self._sig_names = { sig: [name] for (sig, name) in zip(sigs, names) }
+            if len(names) < len(sigs) and len(sigs) != 1:
+                ERR = ("Got {} semicolon-separated names and {} signatures.  " +
+                       "Please provide at least one name per signature line.")
+                raise self.error(ERR.format(len(names), len(sigs)))
+            self._sig_names = { sig: [name] for (sig, name) in zip(sigs, names[:len(sigs)]) }
+            self._sig_names.update({ sigs[0]: [names[0]].append(names[len(sigs):])})
 
     def run(self):
         self._prepare_names()