+ | 0 ->
+ let res = (List.length m1) - (List.length m2) in
+ if res <> 0 then res else Pervasives.compare eq1 eq2
+ | res -> res
+end
+
+(*
+module OrderedEquality = struct
+ type t = Inference.equality
+
+ let minor eq =
+ let w, _, (ty, left, right, o), _ = eq in
+ match o with
+ | Lt -> Some left
+ | Le -> assert false
+ | Gt -> Some right
+ | Ge -> assert false
+ | Eq
+ | Incomparable -> None
+
+ let compare eq1 eq2 =
+ let w1, _, (ty, left, right, o1), m1 = eq1
+ and w2, _, (ty', left', right', o2), m2 = eq2 in
+ match Pervasives.compare w1 w2 with