module Make (T : TermInner.REPR) : sig .. end
exception Fail of (T.t * T.t) list * string
Raised when unification fails. The list of pairs of types is the
unification stack (with the innermost types first)
val unify_exn : T.t -> T.t -> unit
Unify the two types, modifying their binding in place.
Raises Fail if the types are not unifiable
type T.t MetaVar.t ID.Map.t
val free_meta_vars : ?init:meta_vars_set -> T.t -> meta_vars_set
Compute the set of free meta variables that can be bound,
mapped to their meta-variable