Mentions légales du service

Skip to content

[Coq backend] Surjection without matching on int31 literal

Jacques-Henri Jourdan requested to merge coq_no_i31_match into master

Follow-up on !6 (closed)

Instead, we convert the int31 to Z, and perform pattenr matching in Z.

The reason for that change is that pattern-matching on int31 will disappear when native 63 bits integers will be introduced in Coq.

Merge request reports