From 48be18bed2939fdb9b436f282e42a3d636bc50c1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 20 Nov 2016 16:13:33 +0100
Subject: [PATCH] Remove unused parameters from some boxes lemmas.

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

diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index bbefe345f..1d9b5fc94 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -160,7 +160,7 @@ Proof.
     iFrame; eauto.
 Qed.
 
-Lemma box_fill_all f P Q : box N f P ∗ ▷ P ={N}=∗ box N (const true <$> f) P.
+Lemma box_fill_all f P : box N f P ∗ ▷ P ={N}=∗ box N (const true <$> f) P.
 Proof.
   iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
@@ -175,7 +175,7 @@ Proof.
   iApply "Hclose". iNext; iExists true. by iFrame.
 Qed.
 
-Lemma box_empty_all f P Q :
+Lemma box_empty_all f P :
   map_Forall (λ _, (true =)) f →
   box N f P ={N}=∗ ▷ P ∗ box N (const false <$> f) P.
 Proof.
-- 
GitLab