Commit 4e3b4673 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: small fixes

parent 9d80465f
......@@ -354,7 +354,7 @@ let rec t_subst_fmla v t f = t_label_copy f (match f.t_node with
let create_let_decl ld =
let conv_post t q = match t.t_ty with
| Some _ -> open_post_with q t
| Some _ -> open_post_with t q
| None -> let v,f = open_post q in
t_subst_fmla v t f in
let conv_post t ql = (conv_post t) ql in
......@@ -422,11 +422,11 @@ let rec wp_expr env e res q xq = match e.e_node with
let q3 = wp_expr env e3 res q xq in
vc_label e (wp_expr env e1 v (t_if test q2 q3) xq)
| Ecase (e1, bl) ->
let res = res_of_expr e1 in
let v = res_of_expr e1 in
let branch ({pp_pat = pat}, e) =
t_close_branch pat (wp_expr env e res q xq) in
let q = t_case (t_var res) ( branch bl) in
vc_label e (wp_expr env e1 res q xq)
let q = t_case (t_var v) ( branch bl) in
vc_label e (wp_expr env e1 v q xq)
| _ -> assert false (* TODO *)
and sp_expr env e res mpv xmpv = assert (is_fresh res); match e.e_node with
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