Skip to content
Snippets Groups Projects
Commit 55de8385 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix compile

parent 07045934
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/spawn.v
+ 1
− 1
View file @ 55de8385
...@@ -106,7 +106,7 @@ Section spawn. ...@@ -106,7 +106,7 @@ Section spawn.
iIntros "?". by iFrame. } iIntros "?". by iFrame. }
iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let. iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
(* FIXME this is horrible. *) (* FIXME this is horrible. *)
refine (let Hcall := type_call' _ [] [] f' [] [env:expr] refine (let Hcall := type_call' _ [] [] [] f' [env:expr]
(λ _:(), FP_wf ∅ [# fty] retty) in _). (λ _:(), FP_wf ∅ [# fty] retty) in _).
specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()). specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
erewrite of_val_unlock in Hcall; last done. erewrite of_val_unlock in Hcall; last done.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment