sig
  type ty
  type term
  val bind :
    Unif_intf.subst ->
    Unif_intf.S.ty HVar.t Scoped.t ->
    Unif_intf.S.term Scoped.t -> Unif_intf.subst
  val unification :
    ?subst:Unif_intf.subst ->
    Unif_intf.S.term Scoped.t -> Unif_intf.S.term Scoped.t -> Unif_intf.subst
  val matching :
    ?subst:Unif_intf.subst ->
    pattern:Unif_intf.S.term Scoped.t ->
    Unif_intf.S.term Scoped.t -> Unif_intf.subst
  val matching_same_scope :
    ?protect:Unif_intf.S.ty HVar.t Sequence.t ->
    ?subst:Unif_intf.subst ->
    scope:int ->
    pattern:Unif_intf.S.term -> Unif_intf.S.term -> Unif_intf.subst
  val matching_adapt_scope :
    ?protect:Unif_intf.S.ty HVar.t Sequence.t ->
    ?subst:Unif_intf.subst ->
    pattern:Unif_intf.S.term Scoped.t ->
    Unif_intf.S.term Scoped.t -> Unif_intf.subst
  val variant :
    ?subst:Unif_intf.subst ->
    Unif_intf.S.term Scoped.t -> Unif_intf.S.term Scoped.t -> Unif_intf.subst
  val equal :
    subst:Unif_intf.subst ->
    Unif_intf.S.term Scoped.t -> Unif_intf.S.term Scoped.t -> bool
  val are_unifiable : Unif_intf.S.term -> Unif_intf.S.term -> bool
  val matches : pattern:Unif_intf.S.term -> Unif_intf.S.term -> bool
  val are_variant : Unif_intf.S.term -> Unif_intf.S.term -> bool
end