Commit e804f0fa authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: fixed WP for loop (oups)

parent 71677f5f
......@@ -445,10 +445,6 @@ and wp_desc env e q = match e.expr_desc with
let we = wp_expr env e1 q1 in
let we = erase_label env lab we in
let w = match inv with
| None ->
wfr
| Some i ->
wp_and wfr i
| None ->
wp_and wfr (quantify env e.expr_effect we)
| Some 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