diff options
author | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-04-29 23:19:10 -0400 |
---|---|---|
committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-15 12:05:44 -0400 |
commit | 8cc98698e8fc2cf86c5173c2dc0834538a2ca075 (patch) | |
tree | f020f2f5cce4576924649dde22d5bdddad01044c /doc/sphinx/user-extensions | |
parent | a68f75ac6bbd26ef1b6e4ccc635f447a48874220 (diff) |
[doc] Small fixes
Diffstat (limited to 'doc/sphinx/user-extensions')
-rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 16 |
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:: |