sig
  val max_depth : int
  val set_depth : int -> unit
  val set_defs : Sl_defs.t -> unit
  val abd_substs :
    ?used_tags:Tags.t ->
    ?init_state:Sl_unify.Unidirectional.state ->
    ?update_check:Sl_unify.Unidirectional.update_check ->
    ?verify:Sl_unify.Unidirectional.state_check ->
    ?allow_frame:bool ->
    Sl_form.t ->
    Sl_form.t ->
    ((Sl_form.t * Sl_form.t) * Sl_unify.Unidirectional.state list) option
  val abd_bi_substs :
    ?init_state:Sl_unify.Bidirectional.state ->
    ?update_check:Sl_unify.Bidirectional.update_check ->
    ?verify:Sl_unify.Bidirectional.state_check ->
    ?allow_frame:bool ->
    Sl_form.t ->
    Sl_form.t ->
    ((Sl_form.t * Sl_form.t) * Sl_unify.Bidirectional.state list) option
end