in
let module B = NCicBlob.NCicBlob(C) in
let module Pp = Pp.Pp (B) in
- let res,vars = B.embed t in
+ let res = B.embed t in
let module FU = FoUnif.Founif(B) in
- let test_unification vars = function
+ let module IDX = Index.Index(B) in
+ let module Sup = Superposition.Superposition(B) in
+ let test_unification _ = function
| Terms.Node [_; _; lhs; rhs] ->
prerr_endline "Unification test :";
prerr_endline (Pp.pp_foterm lhs);
prerr_endline (Pp.pp_foterm rhs);
- FU.unification vars [] lhs rhs
+ FU.unification [] [] lhs rhs
| _ -> assert false
in
- let subst,vars = test_unification vars res in
+ let subst,vars = test_unification [] res in
prerr_endline "Result :";
prerr_endline (Pp.pp_foterm res);
prerr_endline "Substitution :";