5 files changed, 99 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v
index 2ee438934e..54c75e344c 100644
--- a/test-suite/bugs/closed/2800.v
+++ b/test-suite/bugs/closed/2800.v
@@ -4,3 +4,16 @@ intuition
   match goal with
   | |- _ => idtac " foo"
   end.
+
+  lazymatch goal with _ => idtac end.
+  match goal with _ => idtac end.
+  unshelve lazymatch goal with _ => idtac end.
+  unshelve match goal with _ => idtac end.
+  unshelve (let x := I in idtac).
+Abort.
+
+Require Import ssreflect.
+
+Goal True.
+match goal with _ => idtac end => //.
+Qed.
diff --git a/test-suite/bugs/closed/5500.v b/test-suite/bugs/closed/5500.v
new file mode 100644
index 0000000000..aa63e2ab0e
--- /dev/null
+++ b/test-suite/bugs/closed/5500.v
@@ -0,0 +1,35 @@
+(* Too weak check on the correctness of return clause was leading to an anomaly *)
+
+Inductive Vector A: nat -> Type :=
+  nil: Vector A O
+| cons: forall n, A -> Vector A n -> Vector A (S n).
+
+(* This could be made working with a better inference of inner return
+   predicates from the return predicate at the higher level of the
+   nested matching. Currently, we only check that it does not raise an
+   anomaly, but eventually, the "Fail" could be removed. *)
+
+Fail Definition hd_fst A x n (v: A * Vector A (S n)) :=
+  match v as v0 return match v0 with
+                       (l, r) =>
+                       match r in Vector _ n return match n with 0 => Type | S _ => Type end with
+                         nil _ => A
+                       | cons _ _ _ _ => A
+                       end
+                       end with
+    (_, nil _) => x
+  | (_, cons _ n hd tl) => hd
+  end.
+
+(* This is another example of failure but involving beta-reduction and
+   not iota-reduction. Thus, for this one, I don't see how it could be
+   solved by small inversion, whatever smart is small inversion. *)
+
+Inductive A : (Type->Type) -> Type := J : A (fun x => x).
+
+Fail Check fun x : nat * A (fun x => x) =>
+  match x return match x with
+                 (y,z) => match z in A f return f Type with J => bool end
+                 end with
+  (y,J) => true
+  end.
diff --git a/test-suite/bugs/closed/5547.v b/test-suite/bugs/closed/5547.v
new file mode 100644
index 0000000000..79633f4893
--- /dev/null
+++ b/test-suite/bugs/closed/5547.v
@@ -0,0 +1,16 @@
+(* Checking typability of intermediate return predicates in nested pattern-matching *)
+
+Inductive A : (Type->Type) -> Type := J : A (fun x => x).
+Definition ret (x : nat * A (fun x => x))
+  := match x return Type with
+     | (y,z) => match z in A f return f Type with
+                | J => bool
+                end
+     end.
+Definition foo : forall x, ret x.
+Proof.
+Fail refine (fun x
+          => match x return ret x with
+             | (y,J) => true
+             end
+         ).
diff --git a/test-suite/bugs/closed/7615.v b/test-suite/bugs/closed/7615.v
new file mode 100644
index 0000000000..cd8c4ad7df
--- /dev/null
+++ b/test-suite/bugs/closed/7615.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Module Type S.
+Parameter Inline T@{i} : Type@{i+1}.
+End S.
+
+Module F (X : S).
+Definition X@{j i} : Type@{j} := X.T@{i}.
+End F.
+
+Module M.
+Definition T@{i} := Type@{i}.
+End M.
+
+Module N := F(M).
+
+Require Import Hurkens.
+
+Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl.
diff --git a/test-suite/bugs/closed/7780.v b/test-suite/bugs/closed/7780.v
new file mode 100644
index 0000000000..2318f4d6ec
--- /dev/null
+++ b/test-suite/bugs/closed/7780.v
@@ -0,0 +1,16 @@
+(* A lift was missing in expanding aliases under binders for unification *)
+
+(* Below, the lift was missing while expanding the reference to
+   [mkcons] in [?N] which was under binder [arg] *)
+
+Goal forall T (t : T) (P P0 : T -> Set), option (option (list (P0 t)) -> option (list (P t))).
+  intros ????.
+  refine (Some
+            (fun rls
+             => let mkcons := ?[M] in
+                let default arg := ?[N] in
+                match rls as rls (* 2 *) return option (list (P ?[O])) with
+                | Some _ => None
+                | None => None
+                end)).
+Abort.