From 4ac6047c434872b8b79f56f69f3e8eda6e4206a6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 3 Jan 2017 11:10:16 +0100
Subject: [PATCH] tweak framing
---
theories/typing/own.v | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 60b534d2..1de12dcd 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -64,9 +64,8 @@ Section own.
iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
- iMod (bor_persistent_tok with "LFT EQ Htok") as "[>% Htok]". set_solver.
- iFrame "Htok". iExists l'.
- subst. rewrite heap_mapsto_vec_singleton.
+ iMod (bor_persistent_tok with "LFT EQ Htok") as "[>% $]". set_solver.
+ iExists l'. subst. rewrite heap_mapsto_vec_singleton.
iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
@@ -78,9 +77,9 @@ Section own.
{ apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
{ rewrite bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
- iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ Htok]".
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]".
{ apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
- iFrame "Htok". iApply "Hclose". auto.
+ iApply "Hclose". auto.
- iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
--
GitLab