X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=408a7cdb8904771bc82a0e9f18dc2642ec66c0a1;hb=ff074375003b7b0e3d38e2742ff1d6098a0dab57;hp=8f031a4a7728d2fb44acf33c919fec90fc6b4f78;hpb=b1c222ae8d9bee83d6c5723533a1395d7353893a;p=helm.git

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 8f031a4a7..408a7cdb8 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -243,8 +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 = 0 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)