Bump Iris.

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}%"]

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 :