`iRename` fails with bad error message when not in proof mode (#397) · Issues · Iris / Iris

`iRename` fails with bad error message when not in proof mode

Lemma silly : True.
Proof.
  iRename "H" into "H".

fails with

Unable to unify
 "unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
    (environments.env_spatial ?M11770) ?M11775"
with "True".

The tactic probably does not call iStartProof at the beginning.