Commit a6825e8d authored by Jonas Kastberg's avatar Jonas Kastberg

Bumped to work with Coq 8.10

parent a4707ed5
......@@ -143,7 +143,7 @@ Section sort.
wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (sort_service_func_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
wp_send (A I R) with "[$Hcmp]".
wp_send with "[$Hl]".
wp_recv (ys) as "(Hsorted & Hperm & Hl)".
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