Confusing error msg for `iTimeless`
For example,
Section demo.
Context `{!heapG Σ} (N: namespace).
Lemma foo (P: iProp Σ): inv N P ⊢ WP ref #1 {{ _, True%I }}.
Proof.
iIntros "#?".
iInv N as ">H" "Hclose".
Here, the error info will be
Toplevel input, characters 21-44:
Ltac call to "iInv" failed.
Error: Tactic failure: iTimeless: (▷ P)%I not timeless.
But this is confusing, because the concern is that P
is not timeless, not ▷ P
.