From 80ff25b75839f792add3a66d9896d69f0065c6d8 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 25 May 2018 18:35:30 -0400
Subject: [doc] Allow more than one signature and name per Sphinx object

As discussed in GH-7556.
---
 .../language/gallina-specification-language.rst      | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

(limited to 'doc/sphinx/language')

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}
 
-- 
cgit v1.2.3