Document Rewriting Schemes (quickly).

1 files changed, 4 insertions, 0 deletions

diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 45460bc37..30724759d 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}