Skip to content
Snippets Groups Projects
Commit 476f9e02 authored by Ike Mulder's avatar Ike Mulder
Browse files

Remove superfluous unfolds

parent a15d9e2e
No related branches found
No related tags found
1 merge request!65Fix broken proofs for improved iFrame ∃
Hide whitespace changes
Inline Side-by-side
theories/hocap/concurrent_runners.v
+ 1
− 1
View file @ 476f9e02
...@@ -228,7 +228,7 @@ Section contents. ...@@ -228,7 +228,7 @@ Section contents.
iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv". iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
{ iNext. iLeft. iFrame. } { iNext. iLeft. iFrame. }
wp_pures. iModIntro. iApply "HΦ". wp_pures. iModIntro. iApply "HΦ".
unfold isTask, task. iFrame "#∗". eauto. iFrame "#∗". eauto.
Qed. Qed.
Lemma task_Join_spec γb γ γ' (r t a : val) P Q : Lemma task_Join_spec γb γ γ' (r t a : val) P Q :
......
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