Commit 1a6b6332 authored by David Hauzar's avatar David Hauzar

WP generation bugfix: copying labels of terms corresponding

to branches in if statement.
parent d627ac3f
......@@ -665,8 +665,8 @@ and wp_desc env e q xq = match e.e_node with
| Evalue v -> t_var v.pv_vs
| _ -> raise Exit in
try
let r2 = get_term e2 in
let r3 = get_term e3 in
let r2 = wp_label e2 (get_term e2) in
let r3 = wp_label e3 (get_term e3) in
let v, q = open_post q in
t_subst_single v (t_if_simp test r2 r3) q
with Exit ->
......
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