diff --git a/theories/examples/sort.v b/theories/examples/sort.v index 9a3883958369373fa5b5b8207fc8e4644214d918..1cd272b9c41656de834ca4acbcc1830b76a1c042 100644 --- a/theories/examples/sort.v +++ b/theories/examples/sort.v @@ -143,6 +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. } + (* TODO: This needs explicit (A I R) after Coq 8.10. Figure out why *) wp_send (A I R) with "[$Hcmp]". wp_send with "[$Hl]". wp_recv (ys) as "(Hsorted & Hperm & Hl)".