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

1 files changed, 4 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index d5d721bb2..74aefe490 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