diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 9f7e2faf773f4f0778ab3ce3e271783e0a195281..4e45385768ef31dd842e9e343018fd479b0bafd1 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2023-06-02.4.80f55f7c") | (= "dev") }
+  "coq-iris" { (= "dev.2023-06-04.0.695533ab") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index cf2e327f63426606e8d77aa38d2422a71fdbb8a9..2b3b0f4bc87ae962b09c1fa8a8e160f3bb94966b 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -324,8 +324,8 @@ Proof. split; first done. apply _. Qed.
 Global Instance frame_lft_tok p κ q1 q2 q :
   FrameFractionalQp q1 q2 q →
   Frame p q1.[κ] q2.[κ] q.[κ] | 5.
-(* FIXME: somehow Φ gets inferred wrong here. *)
-Proof. apply: (frame_fractional _ _ _ (λ q, q.[κ])%I). Qed.
+(* FIXME(https://github.com/coq/coq/issues/17688): Φ is not inferred. *)
+Proof. apply: (frame_fractional (λ q, q.[κ])%I). Qed.
 
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
@@ -338,8 +338,8 @@ Proof. split; first done. apply _. Qed.
 Global Instance frame_idx_bor_own p i q1 q2 q :
   FrameFractionalQp q1 q2 q →
   Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
-(* FIXME: somehow Φ gets inferred wrong here. *)
-Proof. apply: (frame_fractional _ _ _ (λ q, idx_bor_own q i)%I). Qed.
+(* FIXME(https://github.com/coq/coq/issues/17688): Φ is not inferred. *)
+Proof. apply: (frame_fractional (λ q, idx_bor_own q i)%I). Qed.
 
 (** Lifetime inclusion *)
 Lemma lft_incl_acc E κ κ' q :