From 6034656d70943b286d90d97e5f761205bc3945a2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 13 Apr 2017 15:04:08 +0200
Subject: [PATCH] Bump Iris.

---
 opam.pins                | 2 +-
 theories/lang/lib/lock.v | 8 ++------
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/opam.pins b/opam.pins
index 069f740a..d2fdcfbf 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1edf71ef9809456c29454d8ad60c34ea10e36fe8
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 55294a275cc03823d941c678d236e36e00b785a5
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 001dbfb5..37cccff3 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -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 [HΦ]"). auto.
+    - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
   Qed.
 
   Lemma release_spec E γ l R P :
-- 
GitLab