diff options
author | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-25 18:35:30 -0400 |
---|---|---|
committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-25 18:35:30 -0400 |
commit | 80ff25b75839f792add3a66d9896d69f0065c6d8 (patch) | |
tree | ae3f16cf4e3f63087ac006c00c63ae57c30917b5 /doc/sphinx/language | |
parent | 8700cee13a137ec0a58f52dc7f75d017e6fbeb19 (diff) |
[doc] Allow more than one signature and name per Sphinx object
As discussed in GH-7556.
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 20 |
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 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} |