From ebe7b443ded3c385b51acaef99944090e577ad94 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Jul 2016 11:50:06 +0200
Subject: [PATCH] Use auth_update_no_frame in boxes.

---
 program_logic/boxes.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 8657892f1..e81180b79 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -70,8 +70,7 @@ Proof.
   rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
   iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
   iApply (@own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
-  rewrite -{1}(right_id ∅ _ (Excl' b2)) -{1}(right_id ∅ _ (Excl' b3)).
-  by apply auth_update, option_local_update, exclusive_local_update.
+  by apply auth_update_no_frame, option_local_update, exclusive_local_update.
 Qed.
 
 Lemma box_own_agree γ Q1 Q2 :
-- 
GitLab