sig
  type state = Sl_subst.t * Tagpairs.t
  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 existential_split_check : state_check
  val modulo_entl : update_check
  val existential_intro : update_check
  val is_substitution : update_check
  val trm_check : update_check
  val avoid_replacing_trms : ?inverse:bool -> Sl_term.Set.t -> update_check
  val avoid_replacing_tags : ?inverse:bool -> Tags.t -> update_check
  val tag_check : update_check
  val existentials_only : update_check
  val unify_tag_constraints :
    ?total:bool ->
    ?inverse:bool -> ?update_check:update_check -> Ord_constraints.t unifier
  val remove_dup_substs : state list -> state list
end