1 files changed, 41 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 41474202..2ce29346 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,31 @@
+Potential sources of incompatibilities between Coq V8.4 and V8.5
+----------------------------------------------------------------
+
+(see also file CHANGES)
+
+Universe Polymorphism.
+
+- Refinement, unification and tactics are now aware of universes,
+  resulting in more localized errors. Universe inconsistencies 
+  should no more get raised at Qed time but during the proof.
+  Unification *always* produces well-typed substitutions, hence
+  some rare cases of unifications that succeeded while producing
+  ill-typed terms before will now fail.
+  
+- The [change p with c] tactic semantics changed, now typechecking 
+  [c] at each matching occurrence [t] of the pattern [p], and 
+  converting [t] with [c].
+  
+- Template polymorphic inductive types: the partial application 
+  of a template polymorphic type (e.g. list) is not polymorphic.
+  An explicit parameter application (e.g [fun A => list A]) or
+  [apply (list _)] will result in a polymorphic instance.
+
+- The type inference algorithm now takes opacity of constants into
+  account. This may have effects on tactics using type inference
+  (e.g. induction). Extra "Transparent" might have to be added to
+  revert opacity of constants.
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
@@ -49,3 +77,16 @@ of the following changes:
 
   - The command "Load" is now atomic for backtracking (use "Unset
     Atomic Load" for compatibility).
+
+
+Incompatibilities beyond 8.4...
+
+- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
+  now "A -> (B <-> C)"
+
+- Tactics: tauto and intuition no longer accidentally destruct binary
+  connectives or records other than and, or, prod, sum, iff. In most
+  of cases, dtauto or dintuition, though stronger than 8.3 tauto and
+  8.3 intuition will provide compatibility.
+
+- "Solve Obligations using" is now "Solve Obligations with".