From 9cb0a6869a23e551b2778ceedeca17c069369c7b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Sep 2020 18:51:50 +0200
Subject: [PATCH] Forwards compatibility fixes with iris!516.

---
 theories/lifetime/model/borrow_sep.v | 6 +++---
 theories/lifetime/model/faking.v     | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 3f17636a..a54b3c8e 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -97,9 +97,9 @@ Proof.
     iDestruct (own_bor_valid_2 with "Hown Hbor2")
         as %[EQB2%to_borUR_included _]%auth_both_valid.
     iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
-    { iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
-      iIntros (->).
-      exfalso. revert Hj1j2. rewrite /= singleton_op singleton_valid.
+    { iIntros (->). iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2.
+      exfalso; revert Hj1j2.
+      rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid.
       by intros [[]]. }
     iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
       as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 668036e2..ae9c563a 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -17,10 +17,10 @@ Proof.
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
   { iModIntro. iExists A, I. by iFrame. }
   iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid.
-  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
-      (frac * agree bor_stateO)))) as (γbor) "[Hbor Hbor']";
-    first by apply auth_both_valid.
-  iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
+  iMod (own_alloc (● (∅ : gmap slice_name
+    (frac * agree bor_stateO)) ⋅ ◯ ∅)) as (γbor) "[Hbor Hbor']".
+  { by apply auth_both_valid. }
+  iMod (own_alloc (● (ε : gset_disj slice_name)))
      as (γinh) "Hinh"; first by apply auth_auth_valid.
   set (γs := LftNames γbor γcnt γinh).
   iMod (own_update with "HI") as "[HI Hγs]".
-- 
GitLab