Skip to content

Compatibility with Coq PR #12984 regarding new reimports of printing rules.

What Coq PR #12984 does is that at re-import time, printing rules which were overriden by intermediate declarations are reactivated (which is a more natural behavior than the previous one).

As indicated in a previous report on the stdpp repository, the Coq PR breaks the heap_lang.v test by reimporting Utf8 on top of bi.weakestpre, so that the "Texan" notations defined there are overriden by the notation defined in Utf8.

The existing reimport of heap_lang.lang in heap_lang.v test does not seem needed anymore. However, reimporting bi.weakestpre helps, what the current Iris MR does.

I don't understand well enough the file organization of iris to be able to tell if this fix is really good. Moreover, it fixes the test file, but I guess that other changes would have to be done to preserve a working environment which prints objects as expected. Reimporting bi.weakestpre might hopefully be enough but I have no idea if this will really be so.

Merge request reports