From 5193311836394d3d18a0187a0d77657aa060b651 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 21 Jun 2016 19:06:30 +0200
Subject: Update CHANGES and COMPATIBILITY

---
 COMPATIBILITY | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'COMPATIBILITY')

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
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3