This may be because you require `ExtrOCamlInt63`

which overrides the extraction of `comparison`

to `int`

, which won't be the case in a future version of Coq. https://github.com/coq/coq/commit/8531e96ad4f47bef39b5890786ed2f1d142b9eca

Li-yao said:

This may be because you require

`ExtrOCamlInt63`

which overrides the extraction of`comparison`

to`int`

, which won't be the case in a future version of Coq. https://github.com/coq/coq/commit/8531e96ad4f47bef39b5890786ed2f1d142b9eca

Extractly, I removed ExtrOCamlInt63 just now, it is fine now~ thanks a lot!

shenghao has marked this topic as resolved.

ah, this is worrying: https://github.com/ocaml/opam-repository/pull/22081

xenstore < 2.1.1 is not compatible with OCaml 5.0 (uses Pervasives)

I have a feeling OCaml 5.0 is going to be a lot of work for everyone in the Coq ecosystem...

Last updated: Feb 06 2023 at 13:03 UTC