Add some compatibility notes on the changes to [change] and unification in general.

2 files changed, 24 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 1847df58e6..8a3cb79d8d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -90,6 +90,9 @@ Tactics
 - "change ... in ..." and "simpl ... in ..." now consider nested
   occurrences (possible source of incompatibilities since this alters
   the numbering of occurrences).
+- 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".
 - Now "appcontext" and "context" behave the same. The old buggy behaviour of
   "context" can be retrieved at parse time by setting the
   "Tactic Compat Context" flag. (possible source of incompatibilities).
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 3c9a94fae2..33bb1d30ee 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,24 @@
+Potential sources of incompatibilities between Coq V8.4 and V8.5
+----------------------------------------------------------------
+
+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.
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------