From 6e4c5345213da1705dc36b89735f3fcccaa0616a Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 7 Apr 2022 17:03:50 +0900
Subject: [PATCH] Minor fix
---
theories/typing/lib/cell.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index a4665d1f..fa0d42a1 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -217,7 +217,7 @@ Section cell.
Proof.
eapply type_fn; [apply _|]=> _ ??[x[]]. simpl_subst.
iIntros (?[?[]]?) "LFT #TIME PROPH UNIQ E Na L C /=[p _] Obs".
- rewrite tctx_hasty_val. iDestruct "p" as ([|d]) "[_ bbox]"=>//.
+ rewrite tctx_hasty_val. iDestruct "p" as ([|d]) "[_ bbox]"=>//.
case x as [[|l|]|]=>//=. rewrite split_mt_ptr. iDestruct "bbox" as "[↦box †]".
wp_bind Skip. iApply (wp_cumulative_time_receipt with "TIME"); [done|].
wp_seq. iIntros "⧗". wp_seq. case d=>// ?.
--
GitLab