1 files changed, 9 insertions, 0 deletions
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
 ===================================