From 9b32c5b01575662249c04bbadef4b6bf3749270c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Apr 2024 14:45:34 +0200
Subject: [PATCH] Bump Iris.

---
 multi_actris/channel/channel.v | 8 ++++----
 multi_actris/channel/proto.v   | 7 +++----
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/multi_actris/channel/channel.v b/multi_actris/channel/channel.v
index 8573236..7e68d81 100644
--- a/multi_actris/channel/channel.v
+++ b/multi_actris/channel/channel.v
@@ -373,10 +373,10 @@ Section channel.
     rewrite iMsg_base_eq.
     iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
     wp_pures.
-    iMod (own_update_2 with "H● H◯") as "[H● H◯]";[apply excl_auth_update|].
-    iModIntro. iApply "HΦ".
-    iFrame. iExists _, _, _, _, _, _. iSplit; [done|].
-    iRewrite "Hp". iFrame "#∗". iApply iProto_le_refl.
+    iMod (own_update_2 with "H● H◯") as "[H● H◯]";
+      [apply (excl_auth_update _ _ (Next p'''))|].
+    iModIntro. iApply "HΦ". rewrite /iProto_pointsto_def. iFrame "IH Hls ∗".
+    iSplit; [done|]. iRewrite "Hp". iApply iProto_le_refl.
   Qed.
 
 End channel.
diff --git a/multi_actris/channel/proto.v b/multi_actris/channel/proto.v
index dea40ec..fdd225f 100644
--- a/multi_actris/channel/proto.v
+++ b/multi_actris/channel/proto.v
@@ -912,8 +912,7 @@ Section proto.
     iSplitL "Hauth".
     - rewrite /iProto_own_auth.
       rewrite map_seq_snoc. simpl. done.
-    - iSplit; [|done].
-      iExists _. iFrame. by iApply iProto_le_refl.
+    - by iApply iProto_le_refl.
   Qed.
 
   Lemma list_lookup_Some_le (ps : list $ iProto Σ V) (i : nat) (p1 : iProto Σ V) :
@@ -1271,7 +1270,7 @@ Section proto.
   Proof.
     iIntros "Hconsistent".
     iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
-    iExists γ. iFrame. iExists _. by iFrame.
+    iExists γ. by iFrame.
   Qed.
 
   Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
@@ -1416,7 +1415,7 @@ Section proto.
 
 End proto.
 
-Typeclasses Opaque iProto_ctx iProto_own.
+Global Typeclasses Opaque iProto_ctx iProto_own.
 
 Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
   first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
-- 
GitLab