Skip to content

Fix a bug in the way we extract Z

Raphaël Cauderlier requested to merge rafoo@fix_Z_extraction into dev

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.

Merge request reports