From 9af73ff6f9721c45e5044ae7dc45dedf9e959545 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 3 Apr 2020 15:59:34 +0200
Subject: [PATCH] more auto-framing
---
theories/base_logic/lib/gc.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/base_logic/lib/gc.v b/theories/base_logic/lib/gc.v
index 801684ea8..691aab0df 100644
--- a/theories/base_logic/lib/gc.v
+++ b/theories/base_logic/lib/gc.v
@@ -155,7 +155,7 @@ Section gc.
Lemma gc_is_gc l v I : gc_mapsto l v I -∗ is_gc_loc l I.
Proof.
- iIntros "Hgc_l". rewrite /gc_mapsto.
+ iIntros "Hgc_l". rewrite /gc_mapsto /is_gc_loc.
(* We need to help Coq type inference... *)
change (V → Prop) with (ofe_car $ leibnizO (V → Prop)) in I.
(* FIXME: is there any good way to avoid repeating the goal here? *)
@@ -224,7 +224,7 @@ Section gc.
{ by apply lookup_to_gc_map_Some in Hsome. }
apply: prod_local_update_1. apply: option_local_update.
apply: exclusive_local_update. done. }
- iDestruct (big_sepM_insert _ _ _ (w, I) with "[Hl HsepM]") as "HsepM"; [ | by iFrame | ].
+ iDestruct (big_sepM_insert _ _ _ (w, I) with "[$HsepM $Hl //]") as "HsepM".
{ apply lookup_delete. }
rewrite insert_delete -to_gc_map_insert. iModIntro. iFrame.
iMod ("Hclose" with "[Hâ— HsepM]"); [ iExists _; by iFrame | by iModIntro].
--
GitLab