Remove custom extraction of comparison to int in ExtrOCamlInt63

[Lysxia]

Fixes #15280

• Added changelog.
• Opened overlay pull requests.

[herbelin]

Cc @vbgl to be sure.

[herbelin]

Cc also @mattam82, since Metacoq had to take into account in {erasure/safechecker}/theories/Extraction.v the choice made by ExtrOCamlInt63.v.

[herbelin]

Then, I guess that it just remains to do an overlay in MetaCoq to change

Extract Constant ascii_compare =>
 "fun x y -> match Char.compare x y with 0 -> Eq | x when x < 0 -> Lt | _ -> Gt".

into

Extract Constant ascii_compare =>
 "fun x y -> match Char.compare x y with 0 -> Eq | x when x < 0 -> Lt | _ -> Gt".

or something like that (I did not double check) in files erasure/theories/Extraction.v, template-coq/theories/Extraction.v and pcuic/theories/Extraction.v. [Edited to fix code]

[herbelin]

Actually, couldn't we add also a

Extract Constant compare =>
 "fun x y -> match Char.compare x y with 0 -> Eq | x when x < 0 -> Lt | _ -> Gt".

in file theories/extraction/ExtrOcamlString.v of the Coq archive.

[Lysxia]

I made the overlay for metacoq; the other CI failures seem unrelated.

Actually, couldn't we add also a
...
in file theories/extraction/ExtrOcamlString.v of the Coq archive.

Let me do that soon in another PR.

[herbelin]

I made the overlay for metacoq; the other CI failures seem unrelated.

Actually, couldn't we add also a
...
in file theories/extraction/ExtrOcamlString.v of the Coq archive.

Let me do that soon in another PR.

OK, then I guess it only remains to make a PR for the overlay.

Assigning.

[Lysxia]

MetaCoq/metacoq#621

[herbelin]

OK, will merge within a couple of hours then.

[herbelin]

@coqbot: merge now

[coqbot-app]

@herbelin: You can't merge the PR because there is no kind: label and no milestone is set.

[herbelin]

@coqbot: merge now

[coqbot-app]

@herbelin: You can't merge the PR because there is no kind: label.

[herbelin]

@coqbot: merge now

[coqbot-app]

@herbelin: Please take care of the following overlays:

• 15294-Lysxia-extract-comparison.sh

[vbgl]

Would it make sense to backport this bugfix to 8.15? Seems easy and might be useful if a 8.15.1 is released before 8.16.0.