aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/user-extensions
diff options
context:
space:
mode:
authorGravatar Clément Pit-Claudel <clement.pitclaudel@live.com>2018-04-29 23:19:10 -0400
committerGravatar Clément Pit-Claudel <clement.pitclaudel@live.com>2018-05-15 12:05:44 -0400
commit8cc98698e8fc2cf86c5173c2dc0834538a2ca075 (patch)
treef020f2f5cce4576924649dde22d5bdddad01044c /doc/sphinx/user-extensions
parenta68f75ac6bbd26ef1b6e4ccc635f447a48874220 (diff)
[doc] Small fixes
Diffstat (limited to 'doc/sphinx/user-extensions')
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst16
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 682553c31..838926d65 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -106,15 +106,15 @@ Automatic declaration of schemes
.. opt:: Elimination Schemes
-It is possible to deactivate the automatic declaration of the
-induction principles when defining a new inductive type with the
-``Unset Elimination Schemes`` command. It may be reactivated at any time with
-``Set Elimination Schemes``.
+ It is possible to deactivate the automatic declaration of the
+ induction principles when defining a new inductive type with the
+ ``Unset Elimination Schemes`` command. It may be reactivated at any time with
+ ``Set Elimination Schemes``.
.. opt:: Nonrecursive Elimination Schemes
-This option controls whether types declared with the keywords :cmd:`Variant` and
-:cmd:`Record` get an automatic declaration of the induction principles.
+ This option controls whether types declared with the keywords :cmd:`Variant` and
+ :cmd:`Record` get an automatic declaration of the induction principles.
.. opt:: Case Analysis Schemes
@@ -125,8 +125,8 @@ This option controls whether types declared with the keywords :cmd:`Variant` and
.. opt:: Decidable Equality Schemes
-These flags control the automatic declaration of those Boolean equalities (see
-the second variant of ``Scheme``).
+ These flags control the automatic declaration of those Boolean equalities (see
+ the second variant of ``Scheme``).
.. warning::