From 89da423547f7dd61bcf59009d6062b3c17f9d8ed Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 Jul 2017 10:23:49 -0700
Subject: [PATCH] fix a comment
---
theories/typing/lib/join.v | 5 +----
1 file changed, 1 insertion(+), 4 deletions(-)
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 532ff66f..40e7c582 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -39,10 +39,7 @@ Section join.
iIntros (_ Ï ret arg). inv_vec arg=>envA envB. simpl_subst.
iApply type_let; [apply HfA|solve_typing|]. iIntros (fA); simpl_subst.
iApply type_let; [apply HfB|solve_typing|]. iIntros (fB); simpl_subst.
- (* Drop to Iris. We handle both function calls in Iris; in principle,
- the call to B could be handled entirely in the type system,
- but we don't seem to have a nice way to frame an Iris assertion
- (here: the join handle) around. *)
+ (* Drop to Iris. *)
iIntros (tid) "#LFT #HE Hna HL Hk (HfB & HfA & HenvA & HenvB & _)".
iMod (lctx_lft_alive_tok Ï with "HE HL") as (qÏ1) "(HÏ1 & HL & Hclose1)"; [solve_typing..|].
(* FIXME: using wp_apply here breaks calling solve_to_val. *)
--
GitLab