Skip to content

drop support for Coq 8.12

Ralf Jung requested to merge ralf/drop-8.12 into master

I am proposing we drop support for Coq 8.12. This is in line with the usual policy of supporting the latest 2 stable releases. Coq 8.13 has been out for half a year, giving a lot of time to port developments.

Requiring Coq 8.13 will let us finally use v closed binder in notation such as big-ops or WP, enabling type annotations. It also lets us land !762 (merged).

Edited by Ralf Jung

Merge request reports