summaryrefslogtreecommitdiff
path: root/test-suite/failure/Case15.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/failure/Case15.v')
-rw-r--r--test-suite/failure/Case15.v11
1 files changed, 7 insertions, 4 deletions
diff --git a/test-suite/failure/Case15.v b/test-suite/failure/Case15.v
index a27b07f8..18faaf5c 100644
--- a/test-suite/failure/Case15.v
+++ b/test-suite/failure/Case15.v
@@ -1,6 +1,9 @@
(* Non exhaustive pattern-matching *)
-Check [x]Cases x x of
- O (S (S y)) => true
- | O (S x) => false
- | (S y) O => true end. \ No newline at end of file
+Check
+ (fun x =>
+ match x, x with
+ | O, S (S y) => true
+ | O, S x => false
+ | S y, O => true
+ end).