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

This is an overlay to be merged synchronously with the upstream PR.

This is an overlay to be merged synchronously with the upstream PR.

No that won't work. We can only land MRs that work with Coq 8.18 and 8.17.

Ah, fun, it's one of those printing changes. And it's hard to normalize away.

I think the best way forward is to for now mark Coq 8.19 as "broken" for our reference file checks, so that the output differences will be ignored. Unfortunately this means we won't notice other regressions in the printed output. When 8.19 becomes stable we can then change the reference files to 8.19 and mark all older Coq versions as "broken".

That does not sound great, but I don't think there's a reasonable alternative.

Having printing output reference files for multiple Coq versions would be possible, but that's a huge hassle. Iris contributors that change tests need to compile with multiple Coq versions to update both .ref files.

mentioned in merge request !1011 (merged)

Superseded by !1011 (merged), so this should not be necessary any more.

closed