aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/user-extensions/proof-schemes.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/user-extensions/proof-schemes.rst')
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst17
1 files changed, 9 insertions, 8 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index e12e4d897..838926d65 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -26,6 +26,7 @@ induction for objects in type `identᵢ`.
natural in case of inductively defined relations.
.. cmdv:: Scheme Equality for @ident
+ :name: Scheme Equality
Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident`
involves some other inductive types, their equality has to be defined first.
@@ -105,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
@@ -124,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::