Commit cfcd6329 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compilation with Coq master.

The `[$]` pattern was used in an ambiguous way; there where multiple
hypotheses that could be used, and for some reason a different is
picked now.
parent a47f27d4
Pipeline #16889 failed with stage
in 10 minutes and 59 seconds
......@@ -273,7 +273,7 @@ Section queue_spec.
{ iExists lh', lt', vs'. iNext. iFrame "Hvs Hlhptr' Hlt Hγe".
destruct vs' as [|v'' vs'']=> //=.
iDestruct "Hlist" as (l) "[Hlh Hlist]". auto with iFrame. }
iModIntro. wp_seq. wp_apply (iron_wp_free with "[$]"); iIntros "_"; wp_seq.
iModIntro. wp_seq. wp_apply (iron_wp_free with "Hlh"). iIntros "_"; wp_seq.
wp_proj. iApply "HΦ". iExists lhptr, ltptr. eauto with iFrame.
Qed.
......
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