+let compute_equality_weight (ty,left,right,o) =
+ let factor = 2 in
+ match o with
+ | Lt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false right) in
+ w + (factor * (List.length m)) ;
+ | Le -> assert false
+ | Gt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false left) in
+ w + (factor * (List.length m)) ;
+ | Ge -> assert false
+ | Eq
+ | Incomparable ->
+ let w1, m1 = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false right) in
+ let w2, m2 = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false left) in
+ (max w1 w2)+(max (factor * (List.length m1)) (factor * (List.length m2)))
+;;
+
+(* old
+let compute_equality_weight (ty,left,right,o) =