Tag release with support for mathcomp 1.15.0

[SnarkBoojum]

I'm updating the mathcomp packages in Debian, and with mathcomp 1.15.0, I get issues with coqeal:

File "./refinements/binrat.v", line 314, characters 34-45:
Error:
In environment
n : BinNums.Z
The term "(1%Z, (n, 1%Z))" has type "(int * (BinNums.Z * int))%type"
while it is expected to have type
 "(BinNums.Z * (BinNums.Z * BinNums.Z))%type".

make[3]: *** [Makefile.coq:763: refinements/binrat.vo] Error 1
make[3]: *** Waiting for unfinished jobs....
File "./refinements/seqpoly.v", line 733, characters 47-48:
Error:
The term "3" has type "GRing.Zmodule.sort ?t"
while it is expected to have type "Equality.sort nat_eqType".

make[3]: *** [Makefile.coq:763: refinements/seqpoly.vo] Error 1
File "./refinements/hpoly.v", line 903, characters 46-47:
Error:
The term "3" has type "GRing.Zmodule.sort ?t"
while it is expected to have type "nat".

I suspect you have already fixed those in git, but there's no official release yet : can you tag one, please? Thanks!

[proux01]

Here it is: https://github.com/coq-community/coqeal/releases (I was waiting for releases of the dependencies finmap and real-closed that just happened)

[SnarkBoojum]

It's uploaded to Debian ; will now be built and made available on various platforms, see here.

[proux01]

Wow, you're faster than me (still have to update Nix) !

[CohenCyril]

Wow, you're faster than me (still have to update Nix) !

I'm already on the nixing

[CohenCyril]

Only the nix packages are all tied together, and now I'm realizing we need a new release of mathcomp-analysis...