summaryrefslogtreecommitdiff
path: root/test-suite/success/Case2.v
blob: db43369503ae6a95301a193447431fde11af10dd (plain)
1
2
3
4
5
6
7
8
9
10
11
12
(* ============================================== *)
(*     To test compilation of dependent case      *)
(*  Nested patterns                               *)
(* ============================================== *)

Type
  match 0 as n return (n = n) with
  | O => refl_equal 0
  | m => refl_equal m
  end.