+let compute_equality_weight ty left right =
+ let metasw = ref 0 in
+ let weight_of t =
+ let w, m = (weight_of_term ~consider_metas:true(* false *) t) in
+(* let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *)
+(* metasw := !metasw + mw; *)
+ metasw := !metasw + (2 * (List.length m));
+ w
+ in
+ (weight_of ty) + (weight_of left) + (weight_of right) + !metasw
+;;
+
+