From 1e1a2f1803c57cc1697e294a7610b76a95661687 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Feb 2015 22:59:41 +0100
Subject: COMPATIBILITY: add note about the change of behavior of Instance foo
 := {| |}. Add test-suite files for closed bugs.

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

(limited to 'COMPATIBILITY')

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 2ce29346c5..3b4e8987c9 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -26,6 +26,13 @@ Universe Polymorphism.
   (e.g. induction). Extra "Transparent" might have to be added to
   revert opacity of constants.
 
+Type classes.
+
+- When writing an Instance foo : Class A := {| proj := t |} (note the
+  vertical bars), support for typechecking the projections using the
+  type information and switching to proof mode is no longer available.
+  Use { } (without the vertical bars) instead.
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3