Fix typo in ConcurrentSeparationLogic.v example

In the 3-stage example, the middle stage moves list elements from the
first stack to the second stack, not back onto the first stack again.
This commit is contained in:
Matthew Dempsky 2020-09-24 13:30:58 -07:00
parent e32105c142
commit 509ebb1d06

View file

@ -699,7 +699,7 @@ Qed.
(* Here's a variant on the last example. Now we have three stages.
* Stage 1: push consecutive even numbers to stack 1.
* Stage 2: pop from stack 1 and push to stack 1, reusing the memory for the
* Stage 2: pop from stack 1 and push to stack 2, reusing the memory for the
* list node.
* Stage 3: pop from stack 2 and fail if odd. *)