Skip to content
Snippets Groups Projects
Commit 6e4c5345 authored by Yusuke Matsushita's avatar Yusuke Matsushita
Browse files

Minor fix

parent 9768082b
No related branches found
No related tags found
No related merge requests found
Pipeline #64377 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/cell.v
+ 1
− 1
View file @ 6e4c5345
......@@ -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=>// ?.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment