From 0a998f837d7d991215f1f2852f9161495bf2b187 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Nov 2023 22:09:29 +0100
Subject: [PATCH] finish mapsto rename
---
theories/lang/heap.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index e77f2782..de766bd7 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -370,7 +370,7 @@ Section heap.
Proof.
intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
assert (Z.to_nat n ≠O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
- iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
+ iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ ?]"; first done.
iMod (own_update _ (â— hF) with "HhF") as "[HhF Hfreeable]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
--
GitLab