From ab4484f7c519f470a1226bd52ded4bb4205c334a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 Aug 2012 17:45:14 +0000
Subject: Some extra INCOMPATIBILITIES since 8.4.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15732 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 COMPATIBILITY | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 41474202aa..3c9a94fae2 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -49,3 +49,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".
-- 
cgit v1.2.3