iAssert without any spatial assumptions should produce a persistent result
The following proof script should work:
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
It currently fails because the update is not persistent -- however, this is an iAssert which is not provided any spatial assertions, so whatever it produces can always be put into the persistent context.
Edited by Ralf Jung