Skip to content
Snippets Groups Projects
Commit 6034656d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 413406e3
No related branches found
No related tags found
No related merge requests found
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1edf71ef9809456c29454d8ad60c34ea10e36fe8
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 55294a275cc03823d941c678d236e36e00b785a5
......@@ -86,13 +86,9 @@ Section proof.
{{{ P }}} acquire [ #l ] @ E {{{ RET #(); locked γ R P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
iPoseProof (try_acquire_spec with "[Hproto] * HP") as "Hacq".
{ iFrame "Hproto". (* FIXME: Just saying "Hproto" in the pattern above should work. *) }
wp_apply "Hacq". (* FIXME: Using `(try_acquire_spec with "[Hproto] * HP")` to avoid the
iPoseProof should work. *)
iIntros ([]).
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
- iIntros "[[Hlked HR] Hown]". wp_if. iApply "HΦ"; iFrame.
- iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown []"). auto.
- iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
Qed.
Lemma release_spec E γ l R P :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment