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 ofcomparison
toint
, 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