diff --git a/theories/examples/sort.v b/theories/examples/sort.v index ed59f992d31e48ac618cbdb1f652bb87b2730ee5..9a3883958369373fa5b5b8207fc8e4644214d918 100644 --- a/theories/examples/sort.v +++ b/theories/examples/sort.v @@ -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.