Find a better name for iMod
We do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
iUpd is my personal favorite. I know that the tactic supports other modalities, but 99,9% of the time it is used to eliminate some form of an update. The name is more informative than
iMod, and not more wrong.
iRun is slightly less informative, but also less wrong: The tactic does bind in a monad, which can be seen as "running the computation".
EDIT: All right, I stand corrected on the "wrong" part. Sorry for that. It is still uninformative.