1 files changed, 9 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index ecbf82e69d..090f7c13be 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,12 @@
+Changes beyond 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
 ==============================