Commit 23202085 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak README more.

parent 1b54ac28
......@@ -31,10 +31,10 @@ correspond to the following parts of the paper:
+ `new_chan_proto_spec`: proof rule for `new_chan`.
+ `send_proto_spec` and `send_proto_spec_packed`: proof rules for `send`, the
first version is more convenient to use in Coq, but otherwise the same as
`send_proto_spec_packed`, which is the rule in the paper.
the latter, which is the rule in the paper.
+ `recv_proto_spec` and `recv_proto_spec_packed`: proof rules for `recv`, the
first version is more convenient to use in Coq, but otherwise the same as
`recv_proto_spec_packed`, which is the rule in the paper.
the latter, which is the rule in the paper.
+ `select_spec`: proof rule for `select`.
+ `branch_spec`: proof rule for `branch`.
......
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