Commit feae9588 authored by Ralf Jung's avatar Ralf Jung

fix build

parent 2649cb67
Pipeline #9921 passed with stage
in 5 minutes and 59 seconds
......@@ -208,6 +208,6 @@ Section stack_works.
{| spec.mk_stack := mk_stack |}.
Next Obligation.
iIntros (????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP").
iIntros "!>" (f f) "Hpop Hpush". iApply "HΦ". iFrame.
iNext. iIntros (f f) "Hpop Hpush". iApply "HΦ". iFrame.
Qed.
End stack_works.
......@@ -625,6 +625,6 @@ Section stack_works.
{| spec.mk_stack := mk_stack |}.
Next Obligation.
iIntros (?????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP").
iIntros "!>" (f f) "#[Hpop Hpush]". iApply "HΦ". iFrame "#".
iNext. iIntros (f f) "#[Hpop Hpush]". iApply "HΦ". iFrame "#".
Qed.
End stack_works.
Markdown is supported
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