diff --git a/theories/vcgen/vcg.v b/theories/vcgen/vcg.v index e88bc47d936933603f681cdff32873ac3ae7d372..cbea760b8dc4188fe48b1ae92c4eee71c55d528e 100644 --- a/theories/vcgen/vcg.v +++ b/theories/vcgen/vcg.v @@ -251,6 +251,8 @@ Section vcg. | _ => wand_denv_interp E m ( ⌜dval_interp E dv1 = #true⌝ ∧ + (* FIXME, make sure that computation of vcg is blocked in the + continuation. *) U (vcg_continuation E (λ E m dv, vcg E n m (dCSeqBind <> de2 (dCWhileV de1 de2)) R Φ) #()) ∨ ⌜dval_interp E dv1 = #false⌝ ∧