Added the computation of max_weight for equations in proofs.

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

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 8f031a4a7728d2fb44acf33c919fec90fc6b4f78..408a7cdb8904771bc82a0e9f18dc2642ec66c0a1 100644 (file)
--- 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)