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).
Proposed alternatives: iRun
, iUpd
. 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.