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).