From df4bb25b5a960b513da59daa10615b9a62de02d2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 28 Nov 2016 10:08:23 +0100
Subject: [PATCH] Improve proof.

---
 theories/lifetime/borrow.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 239a0e22..0d1ed0c2 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -127,8 +127,7 @@ Proof.
         as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
     iMod (box_split with "Hslice Hbox") as (Î³1 Î³2) "(% & % & % & Hs1 & Hs2 & Hbox)".
       solve_ndisj. by rewrite lookup_fmap EQB.
-    iCombine "Hown" "Hbor" as "Hbor". rewrite -own_bor_op.
-    iMod (own_bor_update with "Hbor") as "Hbor".
+    iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
     { etrans; last etrans.
       - apply auth_update_dealloc. by apply delete_singleton_local_update, _.
       - apply auth_update_alloc,
-- 
GitLab