sig
  type state
  val empty_state : Sl_unify.S.state
  type continuation =
      (Sl_unify.S.state, Sl_unify.S.state) Unification.continuation
  type 'a unifier =
      (Sl_unify.S.state, Sl_unify.S.state, 'a) Unification.cps_unifier
  val realize : (Sl_unify.S.state, 'a) Unification.realizer
  type state_check = Sl_unify.S.state Fun.predicate
  val mk_assert_check : Sl_unify.S.state_check -> Sl_unify.S.state_check
  val mk_verifier : Sl_unify.S.state_check -> Sl_unify.S.continuation
  type update_check = Sl_unify.S.state Unification.state_update Fun.predicate
  val unify_tag :
    ?update_check:Sl_unify.S.update_check -> Tags.Elt.t Sl_unify.S.unifier
  val unify_trm :
    ?update_check:Sl_unify.S.update_check -> Sl_term.t Sl_unify.S.unifier
  val unify_trm_list :
    ?update_check:Sl_unify.S.update_check ->
    Sl_term.FList.t Sl_unify.S.unifier
end