stub out the accidentally committed per-location allocation

22cf8bd9 · Ralf Jung · bfbc4420 · 22cf8bd9
Commit 22cf8bd9 authored Feb 14, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

heap_lang/heap.v heap_lang/heap.v +2 -1

No files found.
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -119,7 +119,8 @@ Section heap.
    P ⊑ wp E (Alloc e) Q.
  Proof.
    intros HN ? ? HP. eapply wp_alloc_heap with (σ:=∅); try eassumption.
-    rewrite HP. rewrite left_id.
+    rewrite HP. Fail rewrite left_id.
+  Abort.

  Lemma wp_load_heap N E γ σ l v P Q :
    σ !! l = Some v →