1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v
index 3679eead..6424fe92 100644
--- a/test-suite/success/CaseInClause.v
+++ b/test-suite/success/CaseInClause.v
@@ -20,3 +20,10 @@ Theorem foo : forall (n m : nat) (pf : n = m),
                 match pf in _ = N with 
                   | eq_refl => unit
                 end.
+
+(* Check redundant clause is removed *)
+Inductive I : nat * nat -> Type := C : I (0,0).
+Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end.
+
+(* An example of non-local inference of the type of an impossible case *)
+Check (fun y n (x:Vector.t nat (S n)) => match x with a::_ => a | _ => y end) 2.