X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=c50d809acbd3d4c4bb6515bdedb9d4b07fc000f1;hb=2daf59a983cae8151e513196577ae77b1d12e157;hp=6425e3c82dde87399f88d7277d741be973fcaac6;hpb=536e560bab5e6170f84713b9059ea37527a075b2;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 6425e3c82..c50d809ac 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -419,7 +419,8 @@ let rec demodulation newmeta env table target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
     let res =
-      (C.Implicit None, (eq_ty, left, right, ordering), newmetasenv, newargs)
+      let w = Utils.compute_equality_weight eq_ty left right in
+      (w, (eq_ty, left, right, ordering), newmetasenv, newargs)
     in
     Inference.store_proof res newproof;
     newmeta, res
@@ -602,7 +603,10 @@ let superposition_left (metasenv, context, ugraph) table target =
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
-    let res = (C.Implicit None, (eq_ty, left, right, neworder), [], []) in
+    let res =
+      let w = Utils.compute_equality_weight eq_ty left right in
+      (w, (eq_ty, left, right, neworder), [], [])
+    in
     Inference.store_proof res newproof;
     res
   in
@@ -668,7 +672,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       and newmenv = newmetas @ menv'
       and newargs = args @ args' in
       let eq' =
-        (C.Implicit None, (eq_ty, left, right, neworder), newmenv, newargs)
+        let w = Utils.compute_equality_weight eq_ty left right in
+        (w, (eq_ty, left, right, neworder), newmenv, newargs)
       and env = (metasenv, context, ugraph) in
       let newm, eq' = Inference.fix_metas !maxmeta eq' in
       newm, eq'