Missing error message with `iDestruct ... as "#..."`
Testcase:
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".Prints
No matching clauses for match.That's never an acceptable error message, obviously.