let merge_substs (first: subst) (second: subst) : subst =
if Subst.is_empty first then
second
else if Subst.is_empty second then
first
else
begin
Subst.fold
(fun acc binding ->
let var, term =
binding.Subst.sb_var, binding.Subst.sb_term
in
match Subst.get acc var with
| None ->
(* var is unbound till now, so just keep its binding *)
Subst.append binding acc
| Some acc_term ->
(* this binding does already exists *)
if Subst.term_equal term acc_term then begin
acc
end
(* same variable bound to different terms *)
else
raise (UNIFICATION_FAIL )
)
first
second
end