6 files changed, 67 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/bugs/closed/bug_4869.v b/test-suite/bugs/closed/bug_4869.v
index ac5d7ea287..1fe91de72d 100644
--- a/test-suite/bugs/closed/bug_4869.v
+++ b/test-suite/bugs/closed/bug_4869.v
@@ -6,7 +6,9 @@ Fail Constraint i = Set.
 Constraint Set <= i.
 Constraint Set < i.
 Fail Constraint i < j. (* undeclared j *)
+(* Now a parsing error
 Fail Constraint i < Type. (* anonymous *)
+*)
 
 Set Universe Polymorphism.
 
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.
diff --git a/test-suite/ssr/unfold_fold_polyuniv.v b/test-suite/ssr/unfold_fold_polyuniv.v
new file mode 100644
index 0000000000..1a9309bc79
--- /dev/null
+++ b/test-suite/ssr/unfold_fold_polyuniv.v
@@ -0,0 +1,40 @@
+Require Import ssreflect ssrbool.
+
+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.
+
+Structure type := Pack {sort; op : rel sort}.
+
+Example unfold_fold (T : type) (x : sort T) (a : op T x x) : op T x x.
+Proof.
+  rewrite /op. rewrite -/(op _ _ _). assumption.
+Qed.
+
+Example pattern_unfold_fold (b:bool) (a := b) : paths a b.
+Proof.
+  rewrite [in X in paths X _]/a.
+  rewrite -[in X in paths X _]/a.
+  constructor.
+Qed.
+
+Example unfold_in_hyp (b:bool) (a := b) : unit.
+Proof.
+  assert (paths a a) as A by reflexivity.
+  rewrite [in X in paths X _]/a in A.
+  rewrite /a in (B := idpath a).
+  rewrite [in X in paths _ X]/a in (C := idpath a).
+  constructor.
+Qed.
+
+Example fold_in_hyp (b:bool) (p := idpath b) : unit.
+Proof.
+  assert (paths (idpath b) (idpath b)) as A by reflexivity.
+  rewrite -[in X in paths X _]/p in A.
+  rewrite -[in X in paths _ X]/p in (C := idpath (idpath b)).
+  constructor.
+Qed.