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.
into:
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 Export
s? It will probably make it compatible with the fix of the bug I mentioned above.
Thanks!