From fd342e3210e6a7ad2ed37e72dd5fbd50059eaebc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 3 Apr 2020 15:42:13 +0200
Subject: [PATCH] avoid rewriting with a non-rewritable relation
---
theories/base_logic/lib/gc.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base_logic/lib/gc.v b/theories/base_logic/lib/gc.v
index bea662c03..801684ea8 100644
--- a/theories/base_logic/lib/gc.v
+++ b/theories/base_logic/lib/gc.v
@@ -145,7 +145,7 @@ Section gc.
apply (auth_update_alloc _ (to_gc_map (<[l := (v, I)]> gcm)) (to_gc_map ({[l := (v, I)]}))).
rewrite to_gc_map_insert to_gc_map_singleton.
pose proof (to_gc_map_valid gcm).
- setoid_rewrite alloc_singleton_local_update=>//. }
+ apply: alloc_singleton_local_update; done. }
iMod ("Hclose" with "[Hâ— HsepM Hl]").
+ iExists _.
iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame.
--
GitLab