aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5372.v
blob: 2dc78d4c7f76e684984941e4defaaa30b1485e14 (plain)
1
2
3
4
5
6
7
(* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
Function odd (n:nat) :=
  match n with
  | 0 => false
  | S n => true
  end
with even (n:nat) := false.