coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
121 stars 162 forks source link

coq-mathcomp-classical.1.2.0 (and analysis-1.2.0) works on Coq 8.20 #3121

Closed palmskog closed 1 month ago

palmskog commented 1 month ago

@affeldt-aist FYI.

It would help if you explicitly record Coq as a dependency in both coq-mathcomp-classical and coq-mathcomp-analysis. It turns out that coq-mathcomp-classical.0.7.0 works fine in 8.20, but coq-mathcomp-analysis.0.7.0 does not (due to error on :> inside Class). I leave them both unchanged here.