Commit 585379fb authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue with Coq 8.10.

parent 247dfa43
Pipeline #20559 failed with stage
in 0 seconds
...@@ -300,7 +300,9 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) := ...@@ -300,7 +300,9 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
end; end;
lazymatch goal with lazymatch goal with
| |- False => fail "wp_send:" Hs' "not found" | |- False => fail "wp_send:" Hs' "not found"
| _ => split; [try fast_done|split;[iFrame Hs_frame; solve_done d|wp_finish]] | _ => notypeclasses refine (conj (eq_refl _) (conj _ _));
[iFrame Hs_frame; solve_done d
|wp_finish]
end] end]
| _ => fail "wp_send: not a 'wp'" | _ => fail "wp_send: not a 'wp'"
end end
...@@ -436,7 +438,7 @@ Tactic Notation "wp_select" "with" constr(pat) := ...@@ -436,7 +438,7 @@ Tactic Notation "wp_select" "with" constr(pat) :=
|pm_reduce; |pm_reduce;
lazymatch goal with lazymatch goal with
| |- False => fail "wp_select:" Hs' "not fresh" | |- False => fail "wp_select:" Hs' "not fresh"
| _ => split;[iFrame Hs_frame; solve_done d|wp_finish] | _ => notypeclasses refine (conj _ _); [iFrame Hs_frame; solve_done d|wp_finish]
end] end]
| _ => fail "wp_select: not a 'wp'" | _ => fail "wp_select: not a 'wp'"
end end
......
...@@ -145,8 +145,7 @@ Section sort. ...@@ -145,8 +145,7 @@ Section sort.
wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc". wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)). { rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (sort_service_func_spec with "Hc"); auto. } wp_apply (sort_service_func_spec with "Hc"); auto. }
(* TODO: This needs explicit (A I R) after Coq 8.10. Figure out why *) wp_send with "[$Hcmp]".
wp_send (A I R) with "[$Hcmp]".
wp_send with "[$Hl]". wp_send with "[$Hl]".
wp_recv (ys) as "(Hsorted & Hperm & Hl)". wp_recv (ys) as "(Hsorted & Hperm & Hl)".
wp_pures. iApply "HΦ"; iFrame. wp_pures. iApply "HΦ"; iFrame.
......
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