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

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

diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 51dbdc4d4..2427e9bad 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -161,7 +161,7 @@ Proof.
   iDestruct (box_own_auth_agree γ b true with "[#]")
     as "%"; subst; first by iFrame "Hγ".
   iFrame "HQ".
-  iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
+  iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
     as "[Hγ Hγ']"; first by iFrame "Hγ".
   iPvsIntro; iNext; iSplitL "Hγ"; first (iExists false; by repeat iSplit).
   iExists Φ; iSplit.
@@ -181,7 +181,7 @@ Proof.
   iApply (big_sepM_impl _ _ f); iFrame "Hf".
   iAlways; iIntros {γ b' ?} "[(Hγ' & #$ & #$) HΦ]".
   iInv N as {b} "[Hγ _]"; iTimeless "Hγ".
-  iPvs (box_own_auth_update _ γ b b' true with "[Hγ Hγ']")
+  iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
     as "[Hγ $]"; first by iFrame "Hγ".
   iPvsIntro; iNext; iExists true. by iFrame "HΦ Hγ".
 Qed.
-- 
GitLab