Fix bug #3289

1 files changed, 0 insertions, 21 deletions

diff --git a/test-suite/bugs/opened/3289.v b/test-suite/bugs/opened/3289.v
deleted file mode 100644
index 63453c5b81..0000000000
--- a/test-suite/bugs/opened/3289.v
+++ /dev/null
@@ -1,21 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 1829 lines to 37 lines, then from 47 lines to 18 lines *)
-
-Class Contr_internal (A : Type) :=
-  BuildContr { center : A ;
-               contr : (forall y : A, True) }.
-Class Contr A := Contr_is_contr : Contr_internal A.
-Inductive Unit : Set := tt.
-Instance contr_unit : Contr Unit | 0 :=
-  let x := {|
-        center := tt;
-        contr := fun t : Unit => I
-      |} in x. (* success *)
-
-Fail Instance contr_unit' : Contr Unit | 0 :=
-  {|
-    center := tt;
-    contr := fun t : Unit => I
-  |}.
-(* Error: Mismatched contexts while declaring instance:
- Expected: (Contr_is_contr : Contr_internal _UNBOUND_REL_1)
- Found:   tt  (fun t : Unit => I) *)