Commit c9017ed0 authored by Robbert Krebbers's avatar Robbert Krebbers

Add TODO.

parent 8f46113a
...@@ -251,6 +251,8 @@ Section vcg. ...@@ -251,6 +251,8 @@ Section vcg.
| _ => | _ =>
wand_denv_interp E m ( wand_denv_interp E m (
dval_interp E dv1 = #true dval_interp E dv1 = #true
(* FIXME, make sure that computation of vcg is blocked in the
continuation. *)
U (vcg_continuation E (λ E m dv, U (vcg_continuation E (λ E m dv,
vcg E n m (dCSeqBind <> de2 (dCWhileV de1 de2)) R Φ) #()) vcg E n m (dCSeqBind <> de2 (dCWhileV de1 de2)) R Φ) #())
dval_interp E dv1 = #false dval_interp E dv1 = #false
......
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