From 0268fd31a7d4c8c42846795fd886f72c42ced465 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Sep 2016 22:06:51 +0200
Subject: [PATCH] Tweak.
---
program_logic/thread_local.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index 452b89778..85f075ff9 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -83,8 +83,8 @@ Section proofs.
iIntros "!==>[HP $]".
iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
+ iCombine "Hdis" "Hdis2" as "Hdis".
- iDestruct (own_valid with "Hdis") as %[_ Hval].
- revert Hval. rewrite gset_disj_valid_op. set_solver.
+ iDestruct (own_valid with "Hdis") as %[_ Hval%gset_disj_valid_op].
+ set_solver.
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
- iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame.
set_solver.
--
GitLab