sig
  module type S =
    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
  module Unidirectional :
    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
  module Bidirectional :
    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
end