From af9bc4e4b68a6f179bcff8c450980b12f15892d9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Apr 2016 12:40:54 +0200
Subject: [PATCH] Tweak wp_load.

---
 heap_lang/heap.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 991bd1df9..1b4177494 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -170,7 +170,7 @@ Section heap.
     iFrame "Hmapsto". iIntros {h} "[% Hheap]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hheap". iNext.
-    iIntros "Hheap". iFrame "Hheap". iSplit; first by iPureIntro. done.
+    iIntros "$". by iSplit.
   Qed.
 
   Lemma wp_store N E l v' e v P Î¦ :
-- 
GitLab