;;
+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: