Loop : forall a, a -> (a -> cmd (outcome a)) -> cmd a
However, the operational semantics provided in sections 14.1 and 18.1
invoke the loop body function using "Again(i)" (type "outcome a").
They should instead use simply "i" (type "a").
Changing to "f(i)" also matches the StepLoop formalizations in
SeparationLogic.v and ConcurrentSeparationLogic.v, which invoke simply
"body init" (rather than "body (Again init)").
mdempsky
commented
3 years ago 
In section 13.3, the type of Loop is defined as:
However, the operational semantics provided in sections 14.1 and 18.1 invoke the loop body function using "Again(i)" (type "outcome a"). They should instead use simply "i" (type "a").
Changing to "f(i)" also matches the StepLoop formalizations in SeparationLogic.v and ConcurrentSeparationLogic.v, which invoke simply "body init" (rather than "body (Again init)").