iAlways fails without a proper error message
The following script
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
Fails at iAlways
saying
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last call failed.
No matching clauses for match.
It should either give a proper error or empty the spatial context.