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

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

1 files changed, 27 insertions, 0 deletions

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.