Fix a bug in the way we extract Z
Z
in Coq is defined as Inductive Z := Z0 | Z.pos : positive -> Z | Z.neg : positive -> Z.
. At extraction, we map both Z
and positive
to the OCaml type Z.t
from the Zarith library and we extract match z with Z0 => foo | Z.pos p => bar | Z.neg p => baz end
as Zarith.(if z > zero then bar else if z < zero then baz else foo)
.
This is actually buggy, the positive number p
should be negated in the Z.neg
branch. This MR fixes that.