From 06a2065ef53ffcab185d9f3ddf2dfb204cfb7082 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 19 Dec 2011 19:19:39 +0000
Subject: Notifying removal of accidental unfolding of recursive calls of
 fixpoints by destruct/inversion.

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

diff --git a/CHANGES b/CHANGES
index d5d721bb23..74aefe490c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,7 +32,7 @@ Tactics
 
 - New proof engine.
 - Scripts can now be structured thanks to bullets - * + and to subgoal
-  delimitation via { }. Note : for use with ProofGeneral, a cvs version of
+  delimitation via { }. Note: for use with ProofGeneral, a cvs version of
   ProofGeneral no older than mid-July 2011 is currently required. DOC TODO.
 - Support for tactical "info" is suspended.
 - Support for command "Show Script" is suspended.
@@ -66,6 +66,9 @@ Tactics
   it was formerly generalizing again the goal over the given equality.
 - In Ltac, the "context [...]" syntax has now a variant "appcontext [...]"
   allowing to match partial applications in larger applications.
+- When applying destruct or inversion on a fixpoint hiding an inductive
+  type, recursive calls to the fixpoint now remain folded by default (rare
+  source of incompatibility generally solvable by adding a call to simpl).
 
 Vernacular commands
 
-- 
cgit v1.2.3