From 8df261cabfca799a18b176cbffca49d83a5710a0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 10:35:25 +0200
Subject: [PATCH] Bump Iris (sbi removal).

---
 opam                           |  2 +-
 theories/channel/channel.v     | 10 +++++-----
 theories/channel/proto.v       | 18 ++++++++++--------
 theories/channel/proto_model.v | 16 ++++++++--------
 4 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/opam b/opam
index 934a9a1..48e7874 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-05-18.2.fdda97e8") | (= "dev") }
+  "coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
 ]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index d9c728f..736ab7a 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -96,8 +96,8 @@ Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
   ∃ γ s (l r : loc) (lk : val),
     ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
     is_lock (chan_lock_name γ) lk (∃ vsl vsr,
-      llist sbi_internal_eq l vsl ∗
-      llist sbi_internal_eq r vsr ∗
+      llist internal_eq l vsl ∗
+      llist internal_eq r vsr ∗
       iProto_ctx (chan_proto_name γ) vsl vsr) ∗
     iProto_own (chan_proto_name γ) s p.
 Definition iProto_mapsto_aux : seal (@iProto_mapsto_def). by eexists. Qed.
@@ -184,11 +184,11 @@ Section channel.
     {{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
   Proof.
     iIntros (Φ _) "HΦ". wp_lam.
-    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (l) "Hl".
-    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (r) "Hr".
+    wp_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
+    wp_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
     iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
     wp_apply (newlock_spec (∃ vsl vsr,
-      llist sbi_internal_eq l vsl ∗ llist sbi_internal_eq r vsr ∗
+      llist internal_eq l vsl ∗ llist internal_eq r vsr ∗
       iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
     { iExists [], []. iFrame. }
     iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index bd8aa24..4190a72 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -352,14 +352,16 @@ Section proto.
     destruct (proto_case p) as [|(a&m&?)]; [by left|right].
     by exists a, (IMsg m).
   Qed.
-  Lemma iProto_message_equivI {SPROP : sbi} a1 a2 m1 m2 :
+  Lemma iProto_message_equivI `{!BiInternalEq SPROP} a1 a2 m1 m2 :
     (<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧
       (∀ v lp, iMsg_car m1 v lp ≡ iMsg_car m2 v lp).
   Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
-  Lemma iProto_message_end_equivI {SPROP : sbi} a m : (<a> m) ≡ END ⊢@{SPROP} False.
+  Lemma iProto_message_end_equivI `{!BiInternalEq SPROP} a m :
+    (<a> m) ≡ END ⊢@{SPROP} False.
   Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.
-  Lemma iProto_end_message_equivI {SPROP : sbi} a m : END ≡ (<a> m) ⊢@{SPROP} False.
-  Proof. by rewrite bi.internal_eq_sym iProto_message_end_equivI. Qed.
+  Lemma iProto_end_message_equivI `{!BiInternalEq SPROP} a m :
+    END ≡ (<a> m) ⊢@{SPROP} False.
+  Proof. by rewrite internal_eq_sym iProto_message_end_equivI. Qed.
 
   (** ** Non-expansiveness of operators *)
   Global Instance iMsg_contractive v n :
@@ -444,7 +446,7 @@ Section proto.
     iApply prop_ext; iIntros "!>"; iSplit.
     - iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
       iDestruct "H" as (pdd) "[H #Hpd]".
-      iApply (bi.internal_eq_rewrite); [|done]; iIntros "!>".
+      iApply (internal_eq_rewrite); [|done]; iIntros "!>".
       iRewrite "Hpd". by iRewrite ("IH" $! pdd).
     - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists _.
       rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
@@ -496,7 +498,7 @@ Section proto.
     iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
     iApply prop_ext; iIntros "!>". iSplit.
     - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'".
-      iApply (bi.internal_eq_rewrite); [|done]; iIntros "!>".
+      iApply (internal_eq_rewrite); [|done]; iIntros "!>".
       by iRewrite ("IH" $! p1').
     - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''.
       rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
@@ -544,7 +546,7 @@ Section proto.
   Proof. solve_proper. Qed.
   Global Instance iProto_le_is_except_0 p1 p2 : IsExcept0 (p1 ⊑ p2).
   Proof.
-    rewrite /IsExcept0 /sbi_except_0. iIntros "[H|$]".
+    rewrite /IsExcept0 /bi_except_0. iIntros "[H|$]".
     rewrite iProto_le_unfold /iProto_le_pre. iLeft. by iMod "H".
   Qed.
 
@@ -956,7 +958,7 @@ Section proto.
   Proof.
     iIntros "H● H◯". iDestruct (own_valid_2 with "H● H◯") as "H✓".
     iDestruct (excl_auth_agreeI with "H✓") as "H✓".
-    iDestruct (bi.later_eq_1 with "H✓") as "H✓"; iNext.
+    iDestruct (later_equivI_1 with "H✓") as "H✓"; iNext.
     rewrite /iProto_unfold. assert (∀ p, proto_map iProp_unfold iProp_fold
         (proto_map iProp_fold iProp_unfold p) ≡ p) as help.
     { intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 268a70e..2ec4fab 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -99,7 +99,7 @@ Qed.
 Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
   Inhabited (proto V PROPn PROP) := populate proto_end.
 
-Lemma proto_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
+Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
   ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
 Proof.
@@ -108,20 +108,20 @@ Proof.
     - iIntros "Heq". by iRewrite "Heq".
     - iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
       iRewrite "Heq". by rewrite proto_fold_unfold. }
-  rewrite /proto_message !proto_unfold_fold bi.option_equivI bi.prod_equivI /=.
-  rewrite bi.discrete_eq bi.discrete_fun_equivI.
-  by setoid_rewrite bi.ofe_morO_equivI.
+  rewrite /proto_message !proto_unfold_fold option_equivI prod_equivI /=.
+  rewrite discrete_eq discrete_fun_equivI.
+  by setoid_rewrite ofe_morO_equivI.
 Qed.
-Lemma proto_message_end_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
 Proof.
   trans (proto_unfold (proto_message a m) ≡ proto_unfold proto_end : SPROP)%I.
   { iIntros "Heq". by iRewrite "Heq". }
-  by rewrite /proto_message !proto_unfold_fold bi.option_equivI.
+  by rewrite /proto_message !proto_unfold_fold option_equivI.
 Qed.
-Lemma proto_end_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
-Proof. by rewrite bi.internal_eq_sym proto_message_end_equivI. Qed.
+Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
 
 (** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
 is contractive *)
-- 
GitLab