Even: Coq to OCaml

even.ml

type _ num =
  | Zero : zero num
  | Succ : ('a num) -> 'a plus num
and _ plus = Plus : 'a num -> 'a plus
and zero = [ ]
;;
type _ even =
  | Even_0 : zero num even
  | Even_S : 'a num odd -> 'a plus num even
and _ odd =
  | Odd_S : 'a num even -> 'a plus num odd
;;

even.v

  Inductive even : N -> Prop :=
  | even_0 : even 0
  | even_S n : odd n -> even (n + 1)
  with odd : N -> Prop :=
  | odd_S n : even n -> odd (n + 1).

Even_S (Odd_S Even_0);;
- : zero plus plus num even = Even_S (Odd_S Even_0)