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.