Merge PR #7606: Allow more than one signature and name per Sphinx object

1 files changed, 6 insertions, 14 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 76a016ff64..d3d515949d 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}