diff options
Diffstat (limited to 'test-suite/success/CaseInClause.v')
-rw-r--r-- | test-suite/success/CaseInClause.v | 4 |
1 files changed, 4 insertions, 0 deletions
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. |