search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
29 stars 1 forks source link

Fix compilation with master #94

Closed proux01 closed 8 months ago

pi8027 commented 5 months ago

@proux01 You mean the master branch of Coq, and so I have to do a release now, right? It is a bit difficult to figure it out after 2 months.

proux01 commented 5 months ago

I guess so. I should indeed have put more context (IIRC there was some automation improved in Coq which made // solve more goals and broke algebra-tactics).

And since this means the last release doesn't work with Coq 8.19, now that MC 2.2 is out for Coq 8.19 and considering last release of zify still works, it would be a perfect time to release algebra-tactics.

pi8027 commented 5 months ago

I confirm that the latest release is not compatible with Coq 8.19.