Reliance on `Export` bug
Dear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is an easy way to observe the problem on Coq master: take
algebra.ufrac_auth, and change the first line:
From iris.algebra Require Export auth frac.
From iris.algebra Require Export auth. From iris.algebra Require Export frac.
it will make the proof of
ufrac_auth_agreeN fail because a view starts applying in the wrong direction...
Could you provide some guidance on how to make the file pass with the two separate
Exports? It will probably make it compatible with the fix of the bug I mentioned above.