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
weakestpre.wp_atomic, line 172.