From 4d06337f9f21b62fa15763f8aee0471e78490150 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 5 Jun 2012 16:59:12 +0000
Subject: CHANGES: mention the end of induction principles for records

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

diff --git a/CHANGES b/CHANGES
index 8408db0d9..b0b067e68 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,13 @@
 Changes from V8.4
 =================
 
+Vernacular commands
+
+- The command "Record foo ..." does not generate induction principles
+  (foo_rect, foo_rec, foo_ind) anymore by default (feature wish #2693).
+  A flag "Set/Unset Record Elimination Schemes" allows to change this.
+  The tactic "induction" on a record is now actually doing "destruct".
+
 Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
-- 
cgit v1.2.3