From c9760e26f4616189e9d64f80225ea3c070bcdb42 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 16:20:57 +0200
Subject: [PATCH] Oops, fix 8d1b743e, forgot something.

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

diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index c2c922082..cd6d14f70 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -191,7 +191,7 @@ Lemma box_empty_all f P Q :
 Proof.
   iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
   iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★
-    box_own_prop γ (Φ γ) ★ inv N (box_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]".
+    box_own_prop γ (Φ γ) ★ inv N (box_slice_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]".
   { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
     iAlways; iIntros {γ b ?} "(Hγ' & #$ & #$)".
     assert (true = b) as <- by eauto.
-- 
GitLab