From b24b40c914eaee24ae6faa85a033bdd7ca4afed4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 2 Sep 2010 12:27:16 +0000
Subject: Clarified role of Set Boolean Equality Schemes wrt Set Equality
 Scheme + backport of 13391 from 8.3 to trunk.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13393 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGES b/CHANGES
index d78cd0c960..f0af2bada0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -194,11 +194,11 @@ Vernacular commands
   illustration of wrong commands.
 - Most commands referring to constant (e.g. Print or About) now support
   referring to the constant by a notation string.
-- Made generation of boolean equality automatic for datatypes (use
-  "Unset Boolean Equality Schemes" for deactivation).
-- Made support for automatic generation of case analysis schemes and
-  congruence schemes available to user (governed by options "Unset
-  Case Analysis Schemes" and "Unset Congruence Schemes").
+- New option "Boolean Equality Schemes" to make generation of boolean
+  equality automatic for datatypes (together with option "Decidable
+  Equality Schemes", this replaces deprecated option "Equality Scheme").
+- Made support for automatic generation of case analysis schemes available
+  to user (governed by option "Set Case Analysis Schemes").
 - New command "(Global?) Generalizable [All|No] Variable(s)? ident(s)?" to
   declare which identifiers are generalizable in `{} and `() binders.
 - New command "Print Opaque Dependencies" to display opaque constants in
-- 
cgit v1.2.3