GitLab

• This seemingly useless Require Import confused me quite a bit. In fact, the Import is 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.