More revision before class

SeparationLogic_template.v

@@ -532,7 +532,7 @@ Proof.
   heq; cases ls; cancel.
 Qed.
 
-Theorem linkedList_nonnull : forall p ls,
+Theorem linkedList_nonnull : forall {p ls},
   p <> 0
   -> linkedList p ls === exists x ls' p', [| ls = x :: ls' |] * p |--> [x; p'] * linkedList p' ls'.
 Proof.

frap_book.tex

@@ -3705,17 +3705,17 @@ $$\infer{\smallstep{(h, x \leftarrow c_1; c_2(x))}{(h', x \leftarrow c'_1; c_2(x
 
 $$\infer{\smallstep{(h, \mt{Loop} \; i \; f)}{(h, x \leftarrow f(\mt{Again}(i)); \mt{match} \; x \; \mt{with} \; \mt{Done}(a) \Rightarrow \mt{Return} \; a \mid \mt{Again}(a) \Rightarrow \mt{Loop} \; a \; f)}}{}$$
 
-$$\infer{\smallstep{(h, \mt{Read} \; a)}{(h, v)}}{
+$$\infer{\smallstep{(h, \mt{Read} \; a)}{(h, \mt{Return} \; v)}}{
   \msel{h}{a} = v
 }
-\quad \infer{\smallstep{(h, \mt{Write} \; a \; v')}{(\mupd{h}{a}{v'}, ())}}{
+\quad \infer{\smallstep{(h, \mt{Write} \; a \; v')}{(\mupd{h}{a}{v'}, \mt{Return} \; ())}}{
   \msel{h}{a} = v
 }$$
 
-$$\infer{\smallstep{(h, \mt{Alloc} \; n)}{(\mupd{h}{a}{0^n}, a)}}{
+$$\infer{\smallstep{(h, \mt{Alloc} \; n)}{(\mupd{h}{a}{0^n}, \mt{Return} \; a)}}{
   \dom{h} \cap [a, a+n) = \emptyset
 }
-\quad \infer{\smallstep{(h, \mt{Free} \; a \; n)}{(h - [a, a+n), ())}}{
+\quad \infer{\smallstep{(h, \mt{Free} \; a \; n)}{(h - [a, a+n), \mt{Return} \; ())}}{
 }$$
 
 A few remarks about the last four rules: