Skip to content
Snippets Groups Projects
Commit e12361cf authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] use sigma for parallel var subst

parent 2a9cd45e
No related branches found
No related tags found
No related merge requests found
......@@ -977,13 +977,11 @@ let alpha () =
F.Subst.add_fun sigma compute ; sigma
let subst xs vs =
let bind w x v = Tmap.add (e_var x) v w in
let vmap =
try List.fold_left2 bind Tmap.empty xs vs
with _ -> raise (Invalid_argument "Wp.Lang.Subst.sigma")
in
let sigma = sigma () in
F.Subst.add_map sigma vmap ; sigma
begin
try List.iter2 (fun x v -> F.Subst.add sigma (e_var x) v) xs vs
with Invalid_argument _ -> raise (Invalid_argument "Wp.Lang.Subst.sigma")
end ; sigma
let e_subst f =
let sigma = sigma () in
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment