- let o = Order.compare_terms l r in
- (* CSC: to avoid equations of the form ? -> T that
- can always be applied and that lead to type-checking errors *)
- (match l,r,o with
- Terms.Var _,_,Terms.Gt
- | _,Terms.Var _,Terms.Lt -> assert false
- | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
- Terms.Equation (l, r, ty, Terms.Lt)
- | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
- Terms.Equation (l, r, ty, Terms.Gt)
- | _ -> 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