From b0fe9afb62c21df3b320d7ca13b92b3d60149c3b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 31 May 2019 13:19:13 +0200
Subject: [PATCH] Bump Iris.

---
 theories/encodings/auth_excl.v | 10 +++++-----
 theories/encodings/channel.v   |  8 ++++----
 theories/encodings/stype.v     |  8 ++++----
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/theories/encodings/auth_excl.v b/theories/encodings/auth_excl.v
index 9aa43fe..ddd2611 100644
--- a/theories/encodings/auth_excl.v
+++ b/theories/encodings/auth_excl.v
@@ -38,11 +38,11 @@ Section auth_excl.
     ✓ (● to_auth_excl x ⋅ ◯ to_auth_excl y) -∗ (x ≡ y : iProp Σ).
   Proof.
     iIntros "Hvalid".
-    iDestruct (auth_validI with "Hvalid") as "[Hy Hvalid]"; simpl.
-    iDestruct "Hy" as ([z|]) "Hy"; last first.
-    - by rewrite left_id right_id_L bi.option_equivI /= excl_equivI.
+    iDestruct (auth_both_validI with "Hvalid") as "[_ [Hle Hvalid]]"; simpl.
+    iDestruct "Hle" as ([z|]) "Hy"; last first.
+    - by rewrite bi.option_equivI /= excl_equivI.
     - iRewrite "Hy" in "Hvalid".
-      by rewrite left_id uPred.option_validI /= excl_validI /=.
+      by rewrite uPred.option_validI /= excl_validI /=.
   Qed.
 
   Lemma excl_eq γ x y :
@@ -64,4 +64,4 @@ Section auth_excl.
       eapply exclusive_local_update. done. }
     by rewrite own_op.
   Qed.
-End auth_excl.
\ No newline at end of file
+End auth_excl.
diff --git a/theories/encodings/channel.v b/theories/encodings/channel.v
index 5f9e8dd..fa0ed8a 100644
--- a/theories/encodings/channel.v
+++ b/theories/encodings/channel.v
@@ -121,10 +121,10 @@ Section channel.
     wp_lam.
     wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
     wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
-      as (lsγ) "[Hls Hls']"; first done.
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
-      as (rsγ) "[Hrs Hrs']"; first done.
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
+    { by apply auth_both_valid. }
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
+    { by apply auth_both_valid. }
     iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
     { rewrite /is_list_ref; eauto. }
     iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index dd4528e..bef6153 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -185,11 +185,11 @@ Section stype_specs.
   Proof.
     iIntros "[#Hcctx [Hcol Hcor]]".
     iMod (own_alloc (● (to_stype_auth_excl st) ⋅
-                     â—¯ (to_stype_auth_excl st)))
-      as (lγ) "[Hlsta Hlstf]"; first done.
+                     ◯ (to_stype_auth_excl st))) as (lγ) "[Hlsta Hlstf]".
+    { by apply auth_both_valid_2. }
     iMod (own_alloc (● (to_stype_auth_excl (dual_stype st)) ⋅
-                     â—¯ (to_stype_auth_excl (dual_stype st))))
-      as (rγ) "[Hrsta Hrstf]"; first done.
+                     ◯ (to_stype_auth_excl (dual_stype st)))) as (rγ) "[Hrsta Hrstf]".
+    { by apply auth_both_valid_2. }
     pose (SessionType_name cγ lγ rγ) as stγ.
     iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
     { iNext. rewrite /inv_st. eauto 10 with iFrame. }
-- 
GitLab