From 22cf8bd9ff09f26960ee8d0681048ed734a9c76d Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sun, 14 Feb 2016 10:02:42 +0100 Subject: [PATCH] stub out the accidentally committed per-location allocation --- heap_lang/heap.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/heap_lang/heap.v b/heap_lang/heap.v index 3bb3fbff7..2bbb8c165 100644 --- 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 → -- GitLab