X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.ml;h=408a7cdb8904771bc82a0e9f18dc2642ec66c0a1;hb=f0e52c3d08c0ee4628ad6bbec32ad912dd35a2a4;hp=a27116bc9f007e232f1d1f9856140fea683f6b86;hpb=4313889a915eb0df74bc047f89a7316c8cf4e19c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index a27116bc9..408a7cdb8 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -243,7 +243,8 @@ let find_equalities context proof =
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
-                    let w = compute_equality_weight stat in
+                    (* let w = compute_equality_weight stat in *)
+                    let w = 0 in 
                     let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)