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