From aa9aba96116536d5160802d1355c19f0cf7b57c1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 15 Dec 2016 10:03:35 +0100
Subject: [PATCH] faking non-atomic borrows

---
 theories/lifetime/na_borrow.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 664a6c6f..70f0b33d 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -46,6 +46,12 @@ Section na_bor.
     iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
+  Lemma na_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &na{κ,tid,N}P.
+  Proof.
+    iIntros (?) "#LFT#H†". iApply (bor_na with ">"). done.
+    by iApply (bor_fake with "LFT H†").
+  Qed.
+
 End na_bor.
 
 Typeclasses Opaque na_bor.
-- 
GitLab