From 295af2d4dba611de767a74943d9e7c6297cb2dbc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 31 May 2016 13:30:03 +0200
Subject: [PATCH] boxes: fewer underscores

---
 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 0a4ff670c..51dbdc4d4 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -156,7 +156,7 @@ Proof.
   iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
   iInv N as {b} "(Hγ & #HγQ & HQ)"; iTimeless "Hγ".
   iDestruct (big_sepM_later _ f with "Hf") as "Hf".
-  iDestruct (big_sepM_delete _ f _ true with "Hf")
+  iDestruct (big_sepM_delete _ f with "Hf")
     as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
   iDestruct (box_own_auth_agree γ b true with "[#]")
     as "%"; subst; first by iFrame "Hγ".
-- 
GitLab