diff --git a/tests/heap_lang.v b/tests/heap_lang.v index 4da765fb33c14c57f2ee3a250cc13a447ae01397..f10a57d99adc64b07130a7af2211f5f1e6edb7b7 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -70,6 +70,6 @@ Section ClosedProofs. Proof. iProof. iIntros "! Hσ". iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot. - by iApply heap_e_spec; first by rewrite nclose_nroot. + iApply heap_e_spec; last done ; by rewrite nclose_nroot. Qed. End ClosedProofs.