iMod and evar instantiation
iMod ... as [$ ?] fails even though
iMod ... as [H ?]; iFrame "H" works fine.
@jjourdan suggests it may be related to Coq lazily propagating instantiated evars, and adding a magic tactic that does the propagation in the right point of executing the
iMod could help.