Clarify use of Require
- This seemingly useless
Require Import
confused me quite a bit. In fact, theImport
is a no-op, and what matters are the side-effects of theRequire
. 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 withImport
, where it sometimes re-exported code; this MR might help ensure that Iris does not rely on that bug.