From a2e945d9848cd703bf81821e7b0735a5744ad607 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 10:56:12 +0100
Subject: [PATCH] heap_lang: try to use cancel
---
heap_lang/heap.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 7e517f24b..8bf797ba1 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -116,8 +116,9 @@ Section heap.
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.
- rewrite -of_heap_insert left_id right_id !assoc.
- apply sep_mono_l.
+ rewrite -of_heap_insert left_id right_id.
+ (* FIXME: cancel (auth_own heap_name {[l := Excl v]} -★ Φ (LocV l))%I. *)
+ rewrite !assoc. apply sep_mono_l.
rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
apply later_intro.
--
GitLab