From ff96075aa1472b1c3b0cfee87cc4ffb06e0f1e2b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 24 Nov 2016 23:46:22 +0100
Subject: [PATCH] Next time I will think about committing something that
works...
---
base_logic/lib/boxes.v | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 5cbff7ecd..7cd28246a 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -185,9 +185,7 @@ Proof.
iMod (box_empty with "[$Hslice $Hbox]") as "[$ Hbox]"; try done.
iMod (box_delete_empty with "[$Hslice $Hbox]") as (P') "[Heq Hbox]".
done. by apply lookup_insert.
- iExists P'. rewrite delete_insert. iFrame.
- iMod (box_fill with "[$Hslice $HQ $Hbox]"). done.
- by rewrite insert_insert.
+ iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //.
Qed.
Lemma box_fill_all E f P :
--
GitLab