X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUnif.ml;h=cb3045c1918e9b0c9682e68c939440eb061d5c10;hb=4244a4d70b9ab2fece0ff5b63506f6d323cbfbe2;hp=05fdbe37cdca5b4b301a0e840890cc5337cf173a;hpb=9883f04161a9972f0641dd85faf224b4f2846f05;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 05fdbe37c..cb3045c19 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -25,11 +25,11 @@ let mem2 a b l =
    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