removed first Cic.term from type equality, added an int (weight of the equality)

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 6425e3c82dde87399f88d7277d741be973fcaac6..c50d809acbd3d4c4bb6515bdedb9d4b07fc000f1 100644 (file)
--- 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'