diff --git a/opam.pins b/opam.pins
index 9d0b4a49b0d771649bd7815204bf32cc0cef0036..15d94cd4a1f8d99f6a8e7adab12e6e7a725d0d35 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0429c257e3088cf77c8852a2cbeff2b02671b8b5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f987ca782d1301d319cf6c4ba8e2ab449ebe903a
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index fa9f7b86de2233b68c18a5f5ce986a6e87cf5ca9..680293b6d27bdfe78da91f5ab16dc44ac4aae28b 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -61,12 +61,8 @@ Section proof.
     wp_seq. wp_alloc l vl as "Hl" "H†". inv_vec vl=>x.
     rewrite heap_mapsto_vec_singleton. (* FIXME shouldn't this also compute now, like bigops do? *)
     wp_let. wp_write.
-    iMod (newlock_inplace with "[HR] Hl") as (γ) "?".
-    { (* FIXME: Can we make it so that we can just say "HR" instead of "[HR]", and the
-         later does not matter? Or at least, "$HR" should work.  Why can't we frame
-         below later? *)
-      done. }
-    iApply "HΦ". done.
+    iMod (newlock_inplace with "HR Hl") as (γ) "?".
+    by iApply "HΦ".
   Qed.
 
   Lemma try_acquire_spec γ l R :
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index f1e0c77ef0cb5968d9478c39573cc32cea405b88..62d715c103dd588462f43ced6f1eb57899f21994 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -51,7 +51,8 @@ Lemma bor_or E κ P Q :
   lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
 Proof.
   iIntros (?) "#LFT H". rewrite uPred.or_alt.
-  iMod (bor_exists with "LFT H") as ([]) "H"; auto.
+  (* The (A:=...) is needed due to Coq bug #5458 *)
+  iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
 Qed.
 
 Lemma bor_later E κ P :