From 0029edfa20256eabfe62b5ef7cb0ce246a92ebb8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 5 Jun 2023 09:26:43 +0200
Subject: [PATCH] Bump Iris.

---
 coq-lambda-rust.opam                | 2 +-
 theories/lifetime/model/primitive.v | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 9f7e2faf..4e453857 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 cf2e327f..2b3b0f4b 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 :
-- 
GitLab