- removed Positive and Negative (all is positive)

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

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