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

As discussed in GH-7556.

4 files changed, 27 insertions, 17 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,