1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 10b0f09cf0..90d8b604f1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,8 @@ Tactics
 - Unification in "apply" supports unification of patterns of the form
   ?f x y = g(x,y) (compatibility ensured by using
   "Unset Tactic Pattern Unification").
+- Tactic autorewrite does no longer instantiate pre-existing
+  existential variables (theoretical source of possible incompatibility).
 
 Vernacular commands