Removed negative equations.

[helm.git] / components / tactics / paramodulation / utils.ml

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index 16556588fa9a0dcf1d167f64f4a39ec25b7043fc..db19e87d1d89f77f67ed818df82b625e323da12e 100644 (file)
--- 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