COMPATIBILITY: add note about the change of behavior of Instance foo :=

{| |}. Add test-suite files for closed bugs.

3 files changed, 40 insertions, 0 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 2ce29346c..3b4e8987c 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
 ----------------------------------------------------------------
 
diff --git a/test-suite/bugs/closed/2775.v b/test-suite/bugs/closed/2775.v
new file mode 100644
index 000000000..f1f384bdf
--- /dev/null
+++ b/test-suite/bugs/closed/2775.v
@@ -0,0 +1,6 @@
+Inductive typ : forall (T:Type), list T ->  Type -> Prop :=
+  | Get : forall (T:Type) (l:list T), typ T l T.
+
+
+Derive Inversion inv with 
+(forall (X: Type) (y: list nat), typ nat y X)  Sort Prop.
diff --git a/test-suite/bugs/closed/3978.v b/test-suite/bugs/closed/3978.v
new file mode 100644
index 000000000..26e021e71
--- /dev/null
+++ b/test-suite/bugs/closed/3978.v
@@ -0,0 +1,27 @@
+Require Import Structures.OrderedType.  
+Require Import Structures.OrderedTypeEx.
+
+Module Type M. Parameter X : Type.      
+
+Declare Module Export XOrd : OrderedType
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M.
+
+Module M' : M.
+  Definition X := nat.
+
+  Module XOrd := Nat_as_OT.
+End M'.
+
+Module Type MyOt.
+  Parameter t : Type.
+  Parameter eq : t -> t -> Prop.
+End MyOt.
+
+Module Type M2. Parameter X : Type.      
+
+Declare Module Export XOrd : MyOt
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M2.