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

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

2 files changed, 33 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2775.v b/test-suite/bugs/closed/2775.v
new file mode 100644
index 0000000000..f1f384bdf7
--- /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 0000000000..26e021e719
--- /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.