From 9e64f5850abcd70faf13a3e044d7ddc255e3ba5d Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 23 Dec 2016 12:24:24 +0100
Subject: [PATCH] typing of letcont: allow picking an arbitrary local lifetime
context
---
theories/typing/cont.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 3db8c352..b5a60810 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -23,8 +23,8 @@ Section typing.
Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
(∀ k args, typed_body E L1 (CCtx_iscont k L1 _ T' :: C) (T' args)
(subst' kb k $ subst_v argsb (vmap of_val args) econt)) →
- (∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) →
- typed_body E (L1 ++ L2) C T (let: kb := Rec kb argsb econt in e2).
+ (∀ k, typed_body E L2 (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) →
+ typed_body E L2 C T (let: kb := Rec kb argsb econt in e2).
Proof.
iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
{ simpl. rewrite decide_left. done. }
--
GitLab