iSpecialize on implications behaves inconsistently
In a goal like
"HP" : ■ P
--------------------------------------□
"HPQ" : ■ P → Q
--------------------------------------∗
Q
doing iSpecialize ("HPQ" with "HP")
behaves as expected, but iSpecialize ("HPQ" with "[]")
fails saying
iSpecialize: (■ P → Q)%I not an implication/wand.
Here's a testcase:
Lemma test_plain_impl `{BiPlainly PROP} P Q :
(■ P → (■ P → Q) -∗ Q)%I.
Proof.
iIntros "#HP HPQ".
Fail iSpecialize ("HPQ" with "[]").
Fail iApply "HPQ".
iSpecialize ("HPQ" with "HP"). done.
Qed.