diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 23:22:18 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-14 14:19:07 +0100 |
commit | c43e06c343e2157b839dab8d62fb8345d3238c3c (patch) | |
tree | 77ddbb44c8b8f2a7c624d80157cbcdb178254415 /doc | |
parent | 0bca8c15643e7b5b894b822db4f50bfbbd0858bb (diff) |
Document Record Elimination Schemes.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-sch.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 956f30851..45460bc37 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -127,6 +127,7 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} +\optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} \label{set-nonrecursive-elimination-schemes} @@ -142,6 +143,7 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. +{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}. In addition, the {\tt Case Analysis Schemes} flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the |