diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 11 |
2 files changed, 15 insertions, 21 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. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0236f19490..705d67e6c6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -376,17 +376,14 @@ for records. Here are examples: Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Notations +.. flag:: Printing Notations - To deactivate the printing of all notations, use the command - ``Unset Printing Notations``. To reactivate it, use the command - ``Set Printing Notations``. - - The default is to use notations for printing terms wherever possible. + Controls whether to use notations for printing terms wherever possible. + Default is on. .. seealso:: - :opt:`Printing All` + :flag:`Printing All` To disable other elements in addition to notations. .. _locating-notations: |