From f1b59d0782d9a829db0ff90421031b91efaf4e5d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 May 2019 10:59:43 +0200
Subject: [PATCH] Fix.

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

diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index e6e09aa4..898e1e29 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -235,7 +235,7 @@ Proof.
   iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ V) ∗
     [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' None) ∗  box_own_prop γ (Φ γ) ∗
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
-  { rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
+  { rewrite -big_sepM_sep -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
     iAlways; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (Ho : from_option (⊑ V) False o) by eauto.
     destruct o as [V'|]=>//. rewrite -Ho.
-- 
GitLab