X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=0a7c5cfcc1c82fdb0be718e4ddde26bca391d876;hb=ee9a771a3cf2124ef65906ae75eb0ba7e2e4303b;hp=f69de41f553929765cc3e0cd393211939e38b2e2;hpb=b68e52f889215ce2c21c3d771f59b2d2057d53c1;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index f69de41f5..0a7c5cfcc 100644
--- 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