Commit 3c05b1ae authored by Dan Frumin's avatar Dan Frumin
Browse files

a tiny clean up

parent 5c942d31
......@@ -343,7 +343,7 @@ Section refinement.
(* First the case where no offers is accepted *)
Lemma pop_no_helping_refinement A γo st st' mb lk :
inv stackN (stackInv A γo st st' mb lk) -
(REL pop_st #st #mb
(REL pop_st #st #mb
<<
CG_locked_pop (#st', lk)%V : () + A) -
REL pop_st_no_offer #st #mb pop_st
......
......@@ -539,6 +539,7 @@ Lemma tac_tp_alloc `{relocG Σ} j Δ1 E1 i1 i2 p K' e e' v Q :
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (ref e')
IntoVal e' v
(* TODO use match here as well *)
( l : loc, Δ2,
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' #l)) Δ1 = Some Δ2
......
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