X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=42703045d0019616b041af03fd1031d02ab66f4f;hb=2daf59a983cae8151e513196577ae77b1d12e157;hp=52d99327e8b5d284c143f57f864027026aa71b53;hpb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 52d99327e..42703045d 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -83,6 +83,12 @@ let weight_of_term ?(consider_metas=true) term =
 ;;
 
 
+let compute_equality_weight ty left right =
+  let weight_of t = fst (weight_of_term ~consider_metas:false t) in
+  (weight_of ty) + (weight_of left) + (weight_of right)
+;;
+
+
 (* returns a "normalized" version of the polynomial weight wl (with type
  * weight list), i.e. a list sorted ascending by meta number,
  * from 0 to maxmeta. wl must be sorted descending by meta number. Example: