Merge branch 'shrinkobl' into trunk

1 files changed, 7 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 0f0a7a04bb..63619a55b8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,8 @@ 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.
+  On by default and deprecated. Minor source of incompatibility
+  for code relying on the precise arguments of abstracted proofs.
 - Serious bugs are fixed in tactic "double induction" (source of
   incompatibilities as soon as the inductive types have dependencies in
   the type of their constructors; "double induction" remains however
@@ -48,8 +50,11 @@ Hints
 
 Program
 
-- The "Shrink Obligations" flag now applies to all obligations, not only those
-  solved by the automatic tactic.
+- The "Shrink Obligations" flag now applies to all obligations, not only
+  those solved by the automatic tactic.
+- "Shrink Obligations" is on by default and deprecated. Minor source of
+  incompatibility for code relying on the precise arguments of
+  obligations.
 
 Notations