From e0ed58e702ea89db0d397d66ce0e223ac8ff50a8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 24 Nov 2017 23:27:52 +0100
Subject: Document Rewriting Schemes (quickly).

---
 doc/refman/RefMan-sch.tex | 4 ++++
 1 file changed, 4 insertions(+)

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}
-- 
cgit v1.2.3