From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/success/CaseInClause.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test-suite/success/CaseInClause.v') 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. -- cgit v1.2.3