iIntros on pure implications stopped working
The following proof script used to work, but does not any more:
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
This is probably a regression of the typeclass-based iIntros?
The following proof script used to work, but does not any more:
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
This is probably a regression of the typeclass-based iIntros?