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*)
- B.t Terms.foterm ->
- B.t Terms.foterm ->
- B.t Terms.substitution * Terms.varlist
-
-(*
-val unification:
- Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm ->
- 'a Terms.substitution * Terms.varlist
-
-val matching:
- Terms.varlist -> Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm ->
- 'a Terms.substitution * Terms.varlist
-
-*)
+ val unification:
+ (* global varlist for both terms t1 and t2 *)
+ Terms.varlist ->
+ (* locked variables: if equal to FV(t2) we match t1 with t2*)
+ Terms.varlist ->
+ B.t Terms.foterm ->
+ B.t Terms.foterm ->
+ B.t Terms.substitution * Terms.varlist
end