Avoid relying on `Export` bugs (!312) · Merge requests · Iris / Iris · GitLab

Maxime Dénès requested to merge maximedenes/iris-coq:fix-export into master Sep 10, 2019

See https://github.com/coq/coq/issues/10480 and https://github.com/coq/coq/issues/10474.