From 5d9cb7ad4b3e4ccc77f77456bbb9969c418fcce2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 25 Apr 2016 14:31:11 +0200 Subject: Fixing a "This clause is redundant" error when interpreting the "in" clause of a "match" over an irrefutable pattern. --- test-suite/success/CaseInClause.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v index 3679eead7..599b9566c 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -20,3 +20,7 @@ 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. -- cgit v1.2.3