From 575fdab5df7c861692b19c62c2004c339c8621df Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Sep 2015 11:21:55 +0200
Subject: Listing separately changes from 8.5betas to final 8.5 and further
 changes from final 8.5 to next version.

---
 CHANGES | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/CHANGES b/CHANGES
index 10ec10a5e4..91d5f0baa6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,7 +1,16 @@
 Changes beyond V8.5
 ===================
 
+Tactics
+
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
+- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
+  tactical w.r.t. variables appearing in the body of the proof.
+
+Program
+
+- The "Shrink Obligations" flag now applies to all obligations, not only those
+  solved by the automatic tactic.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
-- 
cgit v1.2.3