diff --git a/opam.pins b/opam.pins
index 069f740a46ceda760db3aaf6af098a5f38445b9a..d2fdcfbfbff8504ea1b82dc8e39b532b4786cfa3 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 001dbfb57ad2151abc45e618f37b130ee79290a3..37cccff316bd7a2aba37202a268a334f6bc82967 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 :