Commit 4827236a authored by Dan Frumin's avatar Dan Frumin
Browse files

Clean up vcg wp store case

parent 9865cb46
...@@ -122,8 +122,8 @@ Section vcg. ...@@ -122,8 +122,8 @@ Section vcg.
| _ => | _ =>
mapsto_wand_list E m ( (l : loc) (v : val), mapsto_wand_list E m ( (l : loc) (v : val),
dval_interp E dv1 = #l dval_interp E dv1 = #l
dloc_interp E (dLocUnknown l) C v l C v
(dloc_interp E (dLocUnknown l) C[LLvl] dval_interp E dv2 - (l C[LLvl] dval_interp E dv2 -
vcg_wp_continuation E Φ (dval_interp E dv2)))%I vcg_wp_continuation E Φ (dval_interp E dv2)))%I
end%I. end%I.
......
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