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