Commit 7f46144d authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added todo detailing Coq 8.10 confusion

parent 202a6080
...@@ -143,6 +143,7 @@ Section sort. ...@@ -143,6 +143,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 (A I R) 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)".
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