aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Case16.v
blob: df15a42836e8956b7dff2aedee6fb0bbb938bdc0 (plain)
1
2
3
4
5
6
7
8
9
10
11
(* Check for redundant clauses *)

Fail Check
  (fun x =>
   match x, x with
   | O, S (S y) => true
   | S _, S (S y) => true
   | _, S (S x) => false
   | S y, O => true
   | _, _ => true
   end).