Specialization (iApply/iMod) often diverges on missing *
When specializing a lemma that contains Iris-level universal quantifiers, if I forget to add the *
to the pattern, the tactic frequently diverges. This is very frustrating as it is not even clear what's wrong, or where the *
has to be added.
If you want, I can create a minimal example. Right now, one way to see this is to remove the *
from the iMod
in weakestpre.wp_atomic
, line 172.