X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=b1fc1c7048a5f9786b75415bac959f38335e0ac4;hb=6b0a195b180e3526af7b55771b2df7b10acd7c30;hp=3206ff7d20bf0977752fa3cac36173cb73c6a2a5;hpb=b97a7976503b2d2e5cbc9199f848135a324775a8;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 3206ff7d2..b1fc1c704 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -7,17 +7,19 @@ let nparamod metasenv subst context t =
   in
   let module B = NCicBlob.NCicBlob(C) in
   let module Pp = Pp.Pp (B) in
-  let res,vars = B.embed t in
-  let module FU = Founif.Founif(B) in
-  let test_unification vars = function
+  let res = B.embed t in
+  let module FU = FoUnif.Founif(B) in
+  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 :";