`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.