diff options
| -rw-r--r-- | doc/refman/RefMan-sch.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 45460bc37a..30724759d2 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -130,6 +130,7 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} +\optindex{Rewriting Schemes} \label{set-nonrecursive-elimination-schemes} } @@ -158,6 +159,9 @@ However 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. +The {\tt Rewriting Schemes} flag governs generation of equality +related schemes such as congruence. + \subsection{\tt Combined Scheme} \label{CombinedScheme} \comindex{Combined Scheme} |