From 73959011dd7ac53b1eb010e3b3615a074c007bef Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Feb 2016 13:51:41 +0100
Subject: [PATCH] fix heap

---
 heap_lang/heap.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 69a018f5c..91987e6fc 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -86,12 +86,14 @@ Section heap.
       apply to_heap_valid. }
     apply pvs_mono, exist_elim=> γ.
     rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
+    rewrite /heap_mapsto_def /heap_name.
     induction σ as [|l v σ Hl IH] using map_ind.
     { rewrite big_sepM_empty; apply True_intro. }
     rewrite to_heap_insert big_sepM_insert //.
     rewrite (map_insert_singleton_op (to_heap σ));
       last rewrite lookup_fmap Hl; auto.
-    by rewrite auth_own_op IH.
+    (* FIXME: investigate why we have to unfold auth_own here. *)
+    by rewrite auth_own_op IH auth_own_eq. 
   Qed.
 
   Context `{heapG Σ}.
-- 
GitLab