Pattern unification algorithm implementation
type subst
= US.t
exception
NotUnifiable
exception
NotInFragment
val eta_expand_otf : subst:subst -> scope:Scoped.scope -> Type.t list -> Type.t list -> T.t -> T.t -> T.t * T.t * Type.t list
val norm_deref : Unif_subst.t -> T.t Scoped.t -> T.t
val unif_simple : ?subst:Subst.t -> scope:int -> T.t -> T.t -> US.t option
val unify_scoped : ?subst:subst -> ?counter:int Pervasives.ref -> T.t Scoped.t -> T.t Scoped.t -> subst