Mczify 1.6.0+2.3+8.18

This is a maintenance release compatible with Mathematical Components 2.3 to 2.5 and Coq/Rocq 8.18 to 9.1.

From this release, the main opam package is called rocq-mathcomp-zify. The old package coq-mathcomp-zify is still provided as its compatibility shim.

Mczify 1.5.0+2.0+8.16

Compatible with Mathematical Components 2.0 and Coq 8.16 to 8.17. The ssrZ library now provides semiring instances for nat¹ and N, and homomorphism instances for Posz,¹ bin_of_nat, nat_of_bin, N.of_nat, N.to_nat, Z.of_nat, and Z.of_N.

1. These instances will also be included in MathComp from its version 2.1. Thus, we expect to eventually remove them from the Mczify library. ↩ ↩²

Mczify 1.4.0+2.0+8.16

This is a maintenance release compatible with Mathematical Components 2.0 and Coq 8.16 to 8.17.

Mczify 1.3.0+1.12+8.13

This is a maintenance release compatible with Mathematical Components 1.12 to 1.16 and Coq 8.13 to 8.17.

Mczify 1.2.0+1.12+8.13

Compatible with Mathematical Components 1.12 to 1.13 and Coq 8.13 to 8.15+rc1. Support for the NatTrec operators and conversions between nat and N or positive has been added.

Mczify 1.1.0+1.12+8.13

Compatible with Mathematical Components 1.12 and Coq 8.13 to 8.14+rc1. The new file ssrZ.v provides a minimal facility for reasoning about the standard integer type Z and for relating Z and int.

Mczify 1.0.0+1.12+8.13

This is the first release of the mczify library, which enables the use of the Micromega tactics for goals stated with the definitions of the Mathematical Components library. Mczify 1.0.0+1.12+8.13 is compatible with MathComp 1.12 and Coq 8.13.