- This seemingly useless
Require Importconfused me quite a bit. In fact, the
Importis a no-op, and what matters are the side-effects of the
Require. Not the most important thing, but it'd be nice to clarify it one way or the other.
Feel free to drop the 2nd commit (with the comment) in case you consider that weird Coq behavior too obvious. Right now, https://github.com/coq/coq/pull/10476 fixed some bugs with
Import, where it sometimes re-exported code; this MR might help ensure that Iris does not rely on that bug.