Commit 1ea712e8 authored by Dan Frumin's avatar Dan Frumin
Browse files

Remove some trailing whitespaces

parent ab6066fe
......@@ -379,7 +379,7 @@ Section properties.
foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ).
Lemma alloc_heap_None σ l vs j1 j2 :
( i, σ !! (l,i) = None)
( i, σ !! (l,i) = None)
j2 < j1 alloc_heap σ l vs j1 !! (l, j2) = None.
Proof.
intros Hσi. revert j1 j2. induction vs as [|v' vs IH]=> j1 j2 ?; csimpl.
......@@ -389,7 +389,7 @@ Section properties.
Qed.
Lemma alloc_heap_lookup σ l vs i j :
( i, σ !! (l,i) = None)
( i, σ !! (l,i) = None)
alloc_heap σ l vs j !! (l, j + i) = ((ULvl,) <$> vs) !! i.
Proof.
intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl.
......@@ -409,7 +409,7 @@ Section properties.
Qed.
Lemma locked_locs_alloc_heap σ l vs j :
( i, σ !! (l,i) = None)
( i, σ !! (l,i) = None)
locked_locs (alloc_heap σ l vs j) = locked_locs σ.
Proof.
intros ?. revert j. induction vs as [|v vs IH]=> j //=.
......
......@@ -210,7 +210,7 @@ Section vcg.
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
(R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match de with
| dCRet de' =>
| dCRet de' =>
match vcg_eval_dexpr de' with
| Some dv => Φ E m dv
| None => vcg_wp_awp_continuation R E de m Φ
......
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