diff options
Diffstat (limited to 'doc/sphinx/user-extensions/proof-schemes.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 25 |
1 files changed, 11 insertions, 14 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index ab1edc0b27..59cad3bea2 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -103,26 +103,23 @@ induction for objects in type `identᵢ`. Automatic declaration of schemes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Elimination Schemes +.. flag:: 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``. + Enables automatic declaration of induction principles when defining a new + inductive type. Defaults to on. -.. opt:: Nonrecursive Elimination Schemes +.. flag:: 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. + Enables automatic declaration of induction principles for types declared with the :cmd:`Variant` and + :cmd:`Record` commands. Defaults to off. -.. opt:: Case Analysis Schemes +.. flag:: Case Analysis Schemes This flag governs the generation of case analysis lemmas for inductive types, - i.e. corresponding to the pattern-matching term alone and without fixpoint. + i.e. corresponding to the pattern matching term alone and without fixpoint. -.. opt:: Boolean Equality Schemes - -.. opt:: Decidable Equality Schemes +.. flag:: Boolean Equality Schemes + Decidable Equality Schemes These flags control the automatic declaration of those Boolean equalities (see the second variant of ``Scheme``). @@ -132,7 +129,7 @@ Automatic declaration of schemes You have to be careful with this option since Coq may now reject well-defined inductive types because it cannot compute a Boolean equality for them. -.. opt:: Rewriting Schemes +.. flag:: Rewriting Schemes This flag governs generation of equality-related schemes such as congruence. |