Commit 169532f7 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 90135749 73997f27
Pipeline #457 passed with stage
__pycache__
build-times.log*
gitlab-extract
......@@ -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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment