Changed the type of compute-equality_weight that now takes also

[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 fdaf68018ee5971516f1be9700ae497cf6bafe4c..07d95ef866aa0ba5c88e6d94e3b8bbebcaafa52c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -698,9 +698,10 @@ let find_equalities context proof =
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
-                    let w = compute_equality_weight ty t1 t2 in
+                    let stat = (ty,t1,t2,o) in
+                    let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+                    let e = (w, proof, stat, newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -710,8 +711,9 @@ let find_equalities context proof =
               let t1 = S.lift index t1 in
               let t2 = S.lift index t2 in
               let o = !Utils.compare_terms t1 t2 in
-              let w = compute_equality_weight ty t1 t2 in
-              let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
+              let stat = (ty,t1,t2,o) in
+              let w = compute_equality_weight stat in
+              let e = (w, BasicProof (C.Rel index), stat, [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -846,17 +848,19 @@ let find_library_equalities dbd context status maxmeta =
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
-                    let w = compute_equality_weight ty t1 t2 in
+                    let stat = (ty,t1,t2,o) in
+                    let w = compute_equality_weight stat in
                     let proof = BasicProof p in
-                    let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+                    let e = (w, proof, stat, newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
               when iseq uri && not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
-              let w = compute_equality_weight ty t1 t2 in
-              let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
+              let stat = (ty,t1,t2,o) in
+              let w = compute_equality_weight stat in
+              let e = (w, BasicProof term, stat, [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -1115,8 +1119,9 @@ let equality_of_term proof term =
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
       let o = !Utils.compare_terms t1 t2 in
-      let w = compute_equality_weight ty t1 t2 in
-      let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
+      let stat = (ty,t1,t2,o) in
+      let w = compute_equality_weight stat in
+      let e = (w, BasicProof proof, stat, [], []) in
       e
   | _ ->
       raise TermIsNotAnEquality