Adapt to https://github.com/coq/coq/pull/18590

added 2 commits

40b3dad0 - Require Coq >= 8.18
f656aeb7 - Adapt to https://github.com/coq/coq/pull/18590

added 2 commits

6e5718a6 - Require Coq >= 8.18
f1db9231 - Adapt to https://github.com/coq/coq/pull/18590

Thanks for the MR. I would be fine to drop support for Coq 8.17 and below.

Please let me know when this is merged. I'll then have a look at the iris overlay (the stdpp/iris setup in Coq's CI (tracking hardcoded refs instead of branches) makes it unpractical to do both overlays at the same time).

We can't drop support for Coq 8.17 before there is a release for Coq 8.19. Then we have to update std++ and Iris to officially support 8.19. Then we have to ensure that none of our other projects still need 8.17. Then we can drop 8.17 from Iris. And then we can drop it from std++.

EDIT: Ah, the 8.19 release happened recently. I can start the update process but it'll take a bit, there's a bunch of manual work involved after each Coq release.

EDIT2: Actually, did the release happen? I don't see a release announcement on Coq-club.

mentioned in merge request iris!1029 (merged)

We have now dropped support for Coq 8.16 and 8.17. (Sorry we didn't merge your MR for this; I prefer to keep such changes completely separate from any other patches, and it's easier to manage these things when I just do the MRs myself.)

Could you rebase this MR? It should then be able to land.

added 7 commits

f1db9231...5dcd0197 - 6 commits from branch iris:master
d8427eec - Adapt to https://github.com/coq/coq/pull/18590

Compare with previous version

resolved all threads

mentioned in commit cafd7113

merged

I have updated iris/examples to fetch the std++ with this patch.

thanks

Adapt to https://github.com/coq/coq/pull/18590

Merge request reports

Activity