Update CHANGES and COMPATIBILITY

2 files changed, 21 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
 
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 883b8576d2..892eaa599e 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,17 @@
+Potential sources of incompatibilities between Coq V8.5 and V8.6
+----------------------------------------------------------------
+
+Symptom: An obligation generated by Program or an abstracted subproof
+has different arguments.
+Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
+and the subproof does not use the argument.
+Remedy:
+- Adapt the script.
+- Write an explicit lemma to prove the obligation/subproof and use it
+  instead (compatible with 8.4).
+- Unset the option for the program/proof the obligation/subproof originates
+  from.
+  
 Potential sources of incompatibilities between Coq V8.4 and V8.5
 ----------------------------------------------------------------