Skip to content

Drop support for Coq versions between v8.10 and v8.13 (included)

Raphaël Cauderlier requested to merge rafoo@drop-support-for-until-v8.13 into dev

There is a change in the way unsigned primitive integers (that we use to represent mutez) are located in Coq Stdlib:

  • in v8.13 and before, they were in a module named Int63.
  • in v8.14, support for signed primitive integers was added and Int63 was splitted into 4 modules: PrimInt63 (logical 63-bit integers), Sint63 (signed ints), Uint63 (unsigned ints), and good old Int63 (a few stuff commons to signed and unsigned integers and a lot of deprecation aliases to Uint63).
  • in v8.15 and v8.16, Int63 is no more.

So it is hard to support both v8.13 (which requires Int63 and does not know about Uint63) and v8.15 (which requires Uint63 and does not know about Int63).

To be more future-proof, we drop support for Coq versions v8.13 and older.

Merge request reports