Skip to content

Support mathcomp 1.11.0 and Coq 8.12

Björn Brandenburg requested to merge coq-8.12 into master

There were a number of breaking changes and a ton of deprecation warnings that this MR fixes. Supporting both mathcomp 1.10.0 and 1.11.0 turned out to require some contortions.

Note: this drops support for mathcomp < 1.10.0 and Coq < 8.11.

CC: @proux @sophie @mlesourd @ptorrx

Merge request reports