From dcfb5aee70549b98a13167aeebc7bc98e63393b2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 6 Dec 2016 11:02:31 +0100
Subject: [PATCH] Curry tl_own_disjoint.

---
 base_logic/lib/thread_local.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/base_logic/lib/thread_local.v b/base_logic/lib/thread_local.v
index 1bcfdee5f..7edacb500 100644
--- a/base_logic/lib/thread_local.v
+++ b/base_logic/lib/thread_local.v
@@ -39,8 +39,9 @@ Section proofs.
   Lemma tl_alloc : (|==> ∃ tid, tl_own tid ⊤)%I.
   Proof. by apply own_alloc. Qed.
 
-  Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 ∗ tl_own tid E2 ⊢ ⌜E1 ⊥ E2⌝.
+  Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 -∗ tl_own tid E2 -∗ ⌜E1 ⊥ E2⌝.
   Proof.
+    apply wand_intro_r.
     rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
   Qed.
 
@@ -85,7 +86,6 @@ Section proofs.
       + iDestruct (own_valid_2 with "Hdis Hdis2") 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.
+    - iDestruct (tl_own_disjoint with "Htoki Htoki2") as %?. set_solver.
   Qed.
 End proofs.
-- 
GitLab