1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 880fa808b..1cce399c3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,8 @@ Changes from V8.1beta to V8.1
   infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })")
 - Support for "where" clause in cofixpoint definitions
 - Support for argument lists of arbitrary length in Tactic Notation
+- [rewrite ... in H] now fails if [H] is used either in an hypohesis
+  or in the goal
 
 Changes from V8.0 to V8.1beta
 =============================