From e4c3055849bc9338bc60fbb342c3e3c8e2b905f4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 31 May 2016 11:21:11 +0200
Subject: [PATCH] make box_fill more symmetric to box_empty

---
 program_logic/boxes.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 625ac17de..0a4ff670c 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -131,16 +131,16 @@ Proof.
   - iExists Φ; by iSplit; [iNext|].
 Qed.
 
-Lemma box_fill f γ b P Q :
-  f !! γ = Some b →
+Lemma box_fill f γ P Q :
+  f !! γ = Some false →
   (box_slice N γ Q ★ ▷ Q ★ ▷ box N f P) ⊢ |={N}=> ▷ box N (<[γ:=true]> f) P.
 Proof.
   iIntros {?} "(#Hinv & HQ & H)"; iDestruct "H" as {Φ} "[#HeqP Hf]".
   iInv N as {b'} "(Hγ & #HγQ & _)"; iTimeless "Hγ".
   iDestruct (big_sepM_later _ f with "Hf") as "Hf".
-  iDestruct (big_sepM_delete _ f _ b with "Hf")
+  iDestruct (big_sepM_delete _ f _ false with "Hf")
     as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
-  iPvs (box_own_auth_update _ γ b' b true with "[Hγ Hγ']")
+  iPvs (box_own_auth_update _ γ b' false true with "[Hγ Hγ']")
     as "[Hγ Hγ']"; first by iFrame "Hγ".
   iPvsIntro; iNext; iSplitL "Hγ HQ"; first (iExists true; by iFrame "Hγ HQ").
   iExists Φ; iSplit.
-- 
GitLab