1 files changed, 0 insertions, 22 deletions
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
deleted file mode 100644
index 9d83743b2a..0000000000
--- a/test-suite/bugs/opened/bug_3890.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Set Nested Proofs Allowed.
-
-Class Foo.
-Class Bar := b : Type.
-
-Set Refine Instance Mode.
-Instance foo : Foo := _.
-Unset Refine Instance Mode.
-(* 1 subgoals, subgoal 1 (ID 4)
-
-  ============================
-   Foo *)
-
-Instance bar : Bar.
-exact Type.
-Defined.
-(* bar is defined *)
-
-About foo.
-(* foo not a defined object. *)
-
-Fail Defined.