aux false false l
;;
-module Founif (B : Terms.Blob) = struct
- module Subst = FoSubst (*.Subst(B)*)
+module Founif (B : Orderings.Blob) = struct
+ module Subst = FoSubst
module U = FoUtils.Utils(B)
- let unification vars locked_vars t1 t2 =
+ let unification (* vars *) locked_vars t1 t2 =
let rec occurs_check subst what where =
match where with
| Terms.Var i when i = what -> true
subst
;;
+(* Sets of variables in s and t are assumed to be disjoint *)
let alpha_eq s t =
let rec equiv subst s t =
let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
in
equiv Subst.id_subst s t
;;
+
end