- raise
- (UnificationFailure (lazy "Inference.unification.unif"))
- | Terms.Var i, t ->
- let subst = Subst.build_subst i t subst in
- subst
- | _, Terms.Var _ -> unif subst t s
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ | Terms.Var i, t -> Subst.build_subst i t subst
+ | t, Terms.Var i when occurs_check subst i t ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ | t, Terms.Var i when (List.mem i locked_vars) ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ | t, Terms.Var i -> Subst.build_subst i t subst