- let o = Order.compare_terms l r in
- Terms.Equation (l, r, ty, o)
- | t -> Terms.Predicate t
+ let o = Order.compare_terms l r in
+ (match l,r,o with
+ Terms.Var _,_,Terms.Gt
+ | _,Terms.Var _,Terms.Lt -> assert false
+ | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
+ true, Terms.Equation (l, r, ty, o)
+ | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
+ true, Terms.Equation (l, r, ty, o)
+ | _ -> false, Terms.Equation (l, r, ty, o))
+ | t -> false,Terms.Predicate t