3 files changed, 24 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v
new file mode 100644
index 0000000000..e1823ac54c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3890.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo.
+
+Instance bar : Bar.
+exact Type.
+Defined.
+
+Defined.
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v
index a8a446cc9b..3f40569d61 100644
--- a/test-suite/bugs/closed/bug_4580.v
+++ b/test-suite/bugs/closed/bug_4580.v
@@ -2,6 +2,5 @@ Require Import Program.
 
 Class Foo (A : Type) := foo : A.
 
-Unset Refine Instance Mode.
 Program Instance f1 : Foo nat := S _.
 Next Obligation. exact 0. Defined.
diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v
new file mode 100644
index 0000000000..951fe5302b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4638.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+
+Goal True.
+
+Instance foo: Foo.
+Qed.
+
+trivial.
+
+Qed.