X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Futils.ml;h=db19e87d1d89f77f67ed818df82b625e323da12e;hb=430fb6e217b6ca61bfc38bb970c1bc57d5643b4c;hp=16556588fa9a0dcf1d167f64f4a39ec25b7043fc;hpb=dbdd5bb6ea9a29c0a06bf29c6ff5db684c8ca0e9;p=helm.git

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index 16556588f..db19e87d1 100644
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -291,7 +291,7 @@ end
 module IntSet = Set.Make(OrderedInt)
 
 let compute_equality_weight (ty,left,right,o) =
-  let factor = 2 in
+  let factor = 1 in
   match o with
     | Lt -> 
 	let w, m = (weight_of_term