Commit 3d01a881 authored by Ralf Jung's avatar Ralf Jung
Browse files

forgot to ammend this...

parent e4a2ae49
Pipeline #202 passed with stage
...@@ -29,6 +29,6 @@ Proof. ...@@ -29,6 +29,6 @@ Proof.
- intros l P. apply ht_alt. - intros l P. apply ht_alt.
by rewrite -(wait_spec heapN N l P) wand_diag right_id. by rewrite -(wait_spec heapN N l P) wand_diag right_id.
- intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //. - intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //.
- intros l P Q. apply recv_strengthen. - intros l P Q. apply recv_weaken.
Qed. Qed.
End spec. End spec.
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