Document side-effects of importing Iris

Iris should have something like std++ has where we document its global, Coq-level side-effects.