From 3f38b1acb2331343436f9f80fd6ffce08eb9a639 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 10 Aug 2023 10:36:21 +0200
Subject: [PATCH] update dependencies

I have no idea why these proofs broke, but they relied on evars in subtle ways so... :shrug:
---
 coq-lambda-rust.opam                 | 2 +-
 theories/lifetime/model/accessors.v  | 4 ++--
 theories/lifetime/model/borrow.v     | 2 +-
 theories/lifetime/model/borrow_sep.v | 4 ++--
 theories/lifetime/model/faking.v     | 2 +-
 theories/lifetime/model/reborrow.v   | 2 +-
 6 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index ea8e14e8..e6211735 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-14.0.f0e415b6") | (= "dev") }
+  "coq-iris" { (= "dev.2023-08-09.1.92e6f4d4") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 971969f6..945816ce 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -212,7 +212,7 @@ Proof.
         iLeft. iFrame "%". iExists _, _. iFrame. }
       iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
       iSplit; first by iApply lft_incl_refl. iExists j. iFrame.
-      iExists Q. rewrite -bi.iff_refl. eauto.
+      iExists Q. rewrite -(bi.iff_refl emp). auto.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
         as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
@@ -262,7 +262,7 @@ Proof.
     rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
     iMod ("Hclose'" with "[- Hâ—¯]"); last first.
     { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
-      iExists j. iFrame. iExists Q. rewrite -bi.iff_refl. auto. }
+      iExists j. iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
     iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
     iLeft. iFrame "%". iExists _, _. iFrame. iNext.
     rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 56adf9af..310bcc83 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -43,7 +43,7 @@ Proof.
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
     + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
-      iExists P. rewrite -bi.iff_refl. auto.
+      iExists P. rewrite -(bi.iff_refl emp). auto.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
       iDestruct ("HIlookup" with "HI") as %Hκ.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 816b02fd..4541525e 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -51,10 +51,10 @@ Proof.
     rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
     iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
-      iFrame. iExists P. rewrite -bi.iff_refl. auto. }
+      iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
     iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
-      iFrame. iExists Q. rewrite -bi.iff_refl. auto. }
+      iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
     iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
     rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index f899d8c2..f0ed43db 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -90,7 +90,7 @@ Proof.
     by do 2 eapply lookup_gset_to_gmap_None. }
   rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
   - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !gset_to_gmap_union_singleton. by iFrame.
-  - iExists γ. iFrame. iExists P. rewrite -bi.iff_refl. eauto.
+  - iExists γ. iFrame. iExists P. rewrite -(bi.iff_refl emp). auto.
 Qed.
 
 Lemma raw_bor_fake' E κ P :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e6cebcce..bb307c2d 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -60,7 +60,7 @@ Proof.
      (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
   iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
-  { iExists j. iFrame. iExists P. rewrite -bi.iff_refl. auto. }
+  { iExists j. iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
   iSplitL "Hbox HB● HB".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
     rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
-- 
GitLab