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

1 files changed, 7 insertions, 0 deletions

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.