1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3890.v b/test-suite/bugs/opened/3890.v
new file mode 100644
index 00000000..f9ac9be2
--- /dev/null
+++ b/test-suite/bugs/opened/3890.v
@@ -0,0 +1,18 @@
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo := _.
+(* 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.