Skip to content

Drop support for Coq 8.8 and 8.9

Ralf Jung requested to merge ci/ralf/drop-8.9 into master

This lets us clean up some little things (see this MR), and it enables some major improvements to gmap and Qp by relying on definitionally proof-irrelevant propositions.

I asked last evening on Mattermost if anyone still uses std++ with such old versions of Coq. So far, nobody responded, but it has been less than 24h. On the other hand, such users can just stick to std++ 1.4.0.

Merge request reports