From 509ebb1d0637c3c7f6e90deffe2a30b4ff7f07b7 Mon Sep 17 00:00:00 2001 From: Matthew Dempsky Date: Thu, 24 Sep 2020 13:30:58 -0700 Subject: [PATCH] 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. --- ConcurrentSeparationLogic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 650d944..4e1c61d 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -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. *)