Commit f6ccb7ff authored by Pietro Abate's avatar Pietro Abate

Fix implementation of unify

parent dd209d29
......@@ -3451,7 +3451,9 @@ module Tallying = struct
) e1 CS.E.empty
in
(* Format.printf "es = %a\n" CS.print_e es; *)
aux ((CS.E.add alpha x sol)) es
let sigma = aux ((CS.E.add alpha x sol)) es in
let talpha = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) sigma x in
CS.E.add alpha talpha sigma
end
in
(* Format.printf "Begin e = %a\n" CS.print_e 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