Removed unused parameter of unification procedure (vars)

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 427db4f95bfca6c911bb5b1f6d9cf5dd786430ef..cb3045c1918e9b0c9682e68c939440eb061d5c10 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -29,7 +29,7 @@ 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

diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli
index 87b57ae70d74b979e83e021cfbae75a95941951e..2371f2180c394cff4d3c19f57aca41c8ab38f2a8 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.mli
+++ b/helm/software/components/ng_paramodulation/foUnif.mli
@@ -17,8 +17,8 @@ module Founif (B : Orderings.Blob) :
   sig
 
    val unification:
-     (* global varlist for both terms t1 and t2 *)
-     Terms.varlist -> 
+     (* global varlist for both terms t1 and t2 (UNUSED) *)
+     (* Terms.varlist -> *)
      (* locked variables: if equal to FV(t2) we match t1 with t2*)
      Terms.varlist -> 
      B.t Terms.foterm ->

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index f69de41f553929765cc3e0cd393211939e38b2e2..0a7c5cfcc1c82fdb0be718e4ddde26bca391d876 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -144,7 +144,7 @@ module Superposition (B : Orderings.Blob) =
                try 
                  let subst =
                    prof_demod_u.HExtlib.profile 
-                     (Unif.unification (varlist@vl) varlist subterm) side 
+                     (Unif.unification (* (varlist@vl) *) varlist subterm) side 
                  in 
                  let side = 
                    prof_demod_s.HExtlib.profile 
@@ -289,7 +289,7 @@ module Superposition (B : Orderings.Blob) =
     let is_identity_clause ~unify = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
       | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
-          (try ignore(Unif.unification vl [] l r); true
+          (try ignore(Unif.unification (* vl *) [] l r); true
           with FoUnif.UnificationFailure _ -> false)
       | _, Terms.Equation (_,_,_,_), _, _ -> false
       | _, Terms.Predicate _, _, _ -> assert false          
@@ -343,7 +343,7 @@ module Superposition (B : Orderings.Blob) =
         | [] -> None
         | (id2,dir,c,vl1)::tl ->
             try
-              let subst = Unif.unification (vl@vl1) locked_vars c t in
+              let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
               Some (id2, dir, subst)
             with FoUnif.UnificationFailure _ -> aux tl
       in
@@ -374,7 +374,7 @@ module Superposition (B : Orderings.Blob) =
           let l = Subst.apply_subst subst l in 
           let r = Subst.apply_subst subst r in 
             try 
-              let subst1 = Unif.unification vl [] l r in
+              let subst1 = Unif.unification (* vl *) [] l r in
               let lit = 
                 match lit with Terms.Predicate _ -> assert false
                   | Terms.Equation (l,r,ty,o) -> 
@@ -627,7 +627,7 @@ module Superposition (B : Orderings.Blob) =
                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
                try 
                  let subst = 
-                   Unif.unification (varlist@vl) [] subterm side 
+                   Unif.unification (* (varlist@vl)*)  [] subterm side 
                  in 
                  if o = Terms.Incomparable then
                    let side = Subst.apply_subst subst side in