module Founif (B : Terms.Blob) :
sig
- val unification:
+ val unification:
(* global varlist for both terms t1 and t2 *)
Terms.varlist ->
(* locked variables: if equal to FV(t2) we match t1 with t2*)
B.t Terms.foterm ->
B.t Terms.substitution * Terms.varlist
+
+ val alpha_eq:
+ B.t Terms.foterm ->
+ B.t Terms.foterm ->
+ B.t Terms.substitution
+
end