Skip to content

GitLab

why3
why3
Commit 41fe3f5a authored by Andrei Paskevich's avatar Andrei Paskevich Committed by Guillaume Melquiond
Browse files
Options

Pmodule: fix a type error in cloning. Fixes #214

parent dda5aa3c
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 2 deletions
src/mlw/pmodule.ml
View file @ 41fe3f5a
...@@ -793,8 +793,8 @@ let rec clone_expr cl sm e = e_attr_copy e (match e.e_node with ...@@ -793,8 +793,8 @@ let rec clone_expr cl sm e = e_attr_copy e (match e.e_node with
e_for v' e_for v'
(e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t)) (e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
i' (clone_invl cl ism invl) (clone_expr cl ism e) i' (clone_invl cl ism invl) (clone_expr cl ism e)
| Eraise (xs, e) -> | Eraise (xs, e1) ->
e_raise (sm_find_xs sm xs) (clone_expr cl sm e) (clone_ity cl e.e_ity) e_raise (sm_find_xs sm xs) (clone_expr cl sm e1) (clone_ity cl e.e_ity)
| Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) -> | Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) ->
let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in
e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e) e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e)
......
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