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

As discussed in GH-7556.

1 files changed, 10 insertions, 1 deletions

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
 ---------