4 files changed, 25 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_10264.v b/test-suite/bugs/closed/bug_10264.v
new file mode 100644
index 0000000000..8351f8325b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10264.v
@@ -0,0 +1,10 @@
+Require Import Program.Tactics.
+
+Definition bla (A:Type) := A.
+Existing Class bla.
+
+Program Instance fubar : bla nat := {}.
+Next Obligation.
+Fail exact bool.
+exact 0.
+Qed.
diff --git a/test-suite/bugs/closed/bug_1618.v b/test-suite/bugs/closed/bug_1618.v
index a7be12e26f..041055a38f 100644
--- a/test-suite/bugs/closed/bug_1618.v
+++ b/test-suite/bugs/closed/bug_1618.v
@@ -20,3 +20,4 @@ a :=
   match a return (P a) with
     | A1 n => f n
   end.
+Proof. Defined.
diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v
index 80c348d207..f1bce04451 100644
--- a/test-suite/bugs/closed/bug_4306.v
+++ b/test-suite/bugs/closed/bug_4306.v
@@ -30,3 +30,5 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
                                 | Gt => y :: foo (xs, ys')
                               end
   end.
+Proof.
+Defined.
diff --git a/test-suite/ssr/case_polyuniv.v b/test-suite/ssr/case_polyuniv.v
new file mode 100644
index 0000000000..8774e191c1
--- /dev/null
+++ b/test-suite/ssr/case_polyuniv.v
@@ -0,0 +1,12 @@
+Require Import ssreflect.
+
+Set Universe Polymorphism.
+
+Cumulative Variant paths {A} (x:A) : A -> Type
+  := idpath : paths x x.
+
+Register paths as core.eq.type.
+Register idpath as core.eq.refl.
+
+Lemma case_test (b:bool) : paths b b.
+Proof. case B:b; reflexivity. Qed.