wp_apply Bad error message when framing in spec pattern fails
Consider this test case:
Lemma frame_fail_test e P Q :
(P -∗ WP e {{ _, True }}) -∗
(Q -∗ WP e {{ _, True }}).
Proof.
iIntros "He HP". wp_apply ("He" with "[$HP]").
It prints Error: No applicable tactic.
, which is not a very useful error message. I would expect it to tell me that HP
could not be framed.