From 8a6c792505160de4ba2123ef049ab45d28873e47 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Oct 2016 17:13:28 +0200
Subject: Allocating a section in CHANGES for changes specific to 8.7.

---
 CHANGES | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 0210281c3a..b2a174c91c 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
-- 
cgit v1.2.3