Permalink
Browse files

Some extra INCOMPATIBILITIES since 8.4.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15732 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
herbelin
herbelin committed Aug 11, 2012
1 parent d71a32d commit ab4484f7c519f470a1226bd52ded4bb4205c334a
Showing with 13 additions and 0 deletions.
  1. +13 −0 COMPATIBILITY
View
@@ -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".

0 comments on commit ab4484f

Please sign in to comment.