GitLab

The following test shows a bad error message:

Lemma test_iSpecialize_auto_frame P Q R :
  (P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.

Error: No applicable tactic.

There is a fail "iSpecialize: premise cannot be solved by framing" in the tactic code but that does not seem to work.