From bbb33095ffa4a84f21b16c3dc79824713b4f0adb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Feb 2016 12:52:52 +0100
Subject: [PATCH] heap: slightly simplify
---
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 82b28a2ee..a6f144390 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -102,7 +102,7 @@ Section heap.
rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
rewrite /wp_fsa -(wp_alloc_pst _ (of_heap h)) //.
apply sep_mono_r; rewrite HP; apply later_mono.
- apply forall_intro=> l; apply wand_intro_l; rewrite (forall_elim l).
+ apply forall_mono=> l; apply wand_intro_l.
rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
rewrite -(exist_intro (op {[ l ↦ Excl v ]})).
repeat erewrite <-exist_intro by apply _; simpl.
--
GitLab