From 647c4a36f2d216063693500e9528494d996440f3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 19 Oct 2017 19:02:59 +0200
Subject: [PATCH] remove True from lft_init

---
 theories/lifetime/lifetime_sig.v | 2 +-
 theories/typing/soundness.v      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index af69eaed..4ac1bd85 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -155,5 +155,5 @@ Module Type lifetime_sig.
   Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
   Parameter lft_init : ∀ `{invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
-    True ={E}=∗ ∃ _ : lftG Σ, lft_ctx.
+    (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
 End lifetime_sig.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 4da62c20..b716b63c 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -36,7 +36,7 @@ Section type_soundness.
     { split. by eapply adequate_nonracing.
       intros. by eapply (adequate_safe (main [exit_cont]%E)). }
     apply: lrust_adequacy=>?. iIntros "_".
-    iMod (lft_init with "[//]") as (?) "#LFT". done.
+    iMod lft_init as (?) "#LFT". done.
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
     iApply (Hmain _ [] [] $! tid with "LFT [] Htl [] []").
-- 
GitLab