update dependencies

I have no idea why these proofs broke, but they relied on evars in subtle ways so... 

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

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).

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κ.

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●".

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 :

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.