1 files changed, 10 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 0210281c3..b2a174c91 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,15 @@
-Changes beyond V8.5
+Changes beyong V8.6
 ===================
 
+Tactics
+
+- New tactic "extensionality in H" which applies (possibly dependent)
+  functional extensionality in H supposed to be a quantified equality
+  until giving a bare equality.
+
+Changes from V8.5 to V8.6beta1
+==============================
+
 Bugfixes
 
 - #4527: when typechecking the statement of a lemma using universe polymorphic