[doc] Allow more than one signature and name per Sphinx object

As discussed in GH-7556.

5 files changed, 42 insertions, 18 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 3036fac81..35a605ddd 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -32,7 +32,16 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
-Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects)::
+
+   .. cmdv:: Lemma @ident {? @binders} : @type
+             Remark @ident {? @binders} : @type
+             Fact @ident {? @binders} : @type
+             Corollary @ident {? @binders} : @type
+             Proposition @ident {? @binders} : @type
+      :name: Lemma; Remark; Fact; Corollary; Proposition
+
+      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
 
 Notations
 ---------
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index f90efa995..f1d2541eb 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -32,7 +32,16 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
-Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects)::
+
+   .. cmdv:: Lemma @ident {? @binders} : @type
+             Remark @ident {? @binders} : @type
+             Fact @ident {? @binders} : @type
+             Corollary @ident {? @binders} : @type
+             Proposition @ident {? @binders} : @type
+      :name: Lemma; Remark; Fact; Corollary; Proposition
+
+      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
 
 Notations
 ---------
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 76a016ff6..d3d515949 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1266,22 +1266,14 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       This feature, called nested proofs, is disabled by default.
       To activate it, turn option :opt:`Nested Proofs Allowed` on.
 
-   The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`:
-
    .. cmdv:: Lemma @ident {? @binders } : @type
-      :name: Lemma
-
-   .. cmdv:: Remark @ident {? @binders } : @type
-      :name: Remark
-
-   .. cmdv:: Fact @ident {? @binders } : @type
-      :name: Fact
-
-   .. cmdv:: Corollary @ident {? @binders } : @type
-      :name: Corollary
+             Remark @ident {? @binders } : @type
+             Fact @ident {? @binders } : @type
+             Corollary @ident {? @binders } : @type
+             Proposition @ident {? @binders } : @type
+      :name: Lemma; Remark; Fact; Corollary; Proposition
 
-   .. cmdv:: Proposition @ident {? @binders } : @type
-      :name: Proposition
+      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
 
 .. cmdv:: Theorem @ident : @type {* with @ident : @type}
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 2b128b98f..88c1e225f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -178,7 +178,7 @@ Sequence
 A sequence is an expression of the following form:
 
 .. tacn:: @expr ; @expr
-   :name: ;
+   :name: ltac-seq
 
    The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be
    a tactic value. The tactic :n:`v__1` is applied to the current goal,
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 8d6e23764..ab3a485b2 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -118,7 +118,7 @@ class CoqObject(ObjectDescription):
             annotation = self.annotation + ' '
             signode += addnodes.desc_annotation(annotation, annotation)
         self._render_signature(signature, signode)
-        return self.options.get("name") or self._name_from_signature(signature)
+        return self._names.get(signature) or self._name_from_signature(signature)
 
     def _record_name(self, name, target_id):
         """Record a name, mapping it to target_id
@@ -176,8 +176,22 @@ class CoqObject(ObjectDescription):
             if report == "warning":
                 raise self.warning(msg)
 
+    def _prepare_names(self):
+        sigs = self.get_signatures()
+        names = self.options.get("name")
+        if names is None:
+            self._names = {}
+        else:
+            names = [n.strip() for n in names.split(";")]
+            if len(names) != len(sigs):
+                ERR = ("Expected {} semicolon-separated names, got {}.  " +
+                       "Please provide one name per signature line.")
+                raise self.error(ERR.format(len(names), len(sigs)))
+            self._names = dict(zip(sigs, names))
+
     def run(self):
         self._warn_if_undocumented()
+        self._prepare_names()
         return super().run()
 
 class PlainObject(CoqObject):