- let _, (ty, left, right, _), _, _ = eq1
- and _, (ty', left', right', _), _, _ = eq2 in
-(* let w1, m1 = weight_of_equality eq1 *)
-(* and w2, m2 = weight_of_equality eq2 in *)
- let weight_of t = fst (weight_of_term ~consider_metas:false t) in
- let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
- and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+ let w1, _, (ty, left, right, _), _, a = eq1
+ and w2, _, (ty', left', right', _), _, a' = eq2 in
+(* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
+(* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
+(* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)