Dropping support for Coq 8.10
At some point we should drop support for Coq 8.10.
The benefits are:
- Ltac2 is available starting with Coq 8.11. This would let us integrate https://gitlab.mpi-sws.org/iris/string-ident into Iris and support the
"%H"intro pattern without any additional work from the user. - Custom entries had some bugs that seem to block their use in !554 (merged); in Coq 8.11 and forward we can give good notation for dfracs.
We should probably release Iris 3.4 before dropping support. Before that out of the current MRs I think !572 (merged) is the most important, to avoid releasing the mnat library and then immediately renaming it.