sig
  type 'a var
  type 'a mvar = 'Bindlib.var array
  type (-'a, +'b) binder
  type ('a, 'b) mbinder
  val subst : ('a, 'b) Bindlib.binder -> '-> 'b
  val msubst : ('a, 'b) Bindlib.mbinder -> 'a array -> 'b
  val new_var : ('Bindlib.var -> 'a) -> string -> 'Bindlib.var
  val new_mvar : ('Bindlib.var -> 'a) -> string array -> 'Bindlib.mvar
  val name_of : 'Bindlib.var -> string
  val uid_of : 'Bindlib.var -> int
  val unbind :
    ('Bindlib.var -> 'a) -> ('a, 'b) Bindlib.binder -> 'Bindlib.var * 'b
  val unbind2 :
    ('Bindlib.var -> 'a) ->
    ('a, 'b) Bindlib.binder ->
    ('a, 'c) Bindlib.binder -> 'Bindlib.var * 'b * 'c
  val eq_binder :
    ('Bindlib.var -> 'a) ->
    ('-> '-> bool) ->
    ('a, 'b) Bindlib.binder -> ('a, 'b) Bindlib.binder -> bool
  val unmbind :
    ('Bindlib.var -> 'a) ->
    ('a, 'b) Bindlib.mbinder -> 'Bindlib.mvar * 'b
  val unmbind2 :
    ('Bindlib.var -> 'a) ->
    ('a, 'b) Bindlib.mbinder ->
    ('a, 'c) Bindlib.mbinder -> 'Bindlib.mvar * 'b * 'c
  val eq_mbinder :
    ('Bindlib.var -> 'a) ->
    ('-> '-> bool) ->
    ('a, 'b) Bindlib.mbinder -> ('a, 'b) Bindlib.mbinder -> bool
  type +'a bindbox
  val box_of_var : 'Bindlib.var -> 'Bindlib.bindbox
  val box : '-> 'Bindlib.bindbox
  val apply_box :
    ('-> 'b) Bindlib.bindbox -> 'Bindlib.bindbox -> 'Bindlib.bindbox
  val box_apply : ('-> 'b) -> 'Bindlib.bindbox -> 'Bindlib.bindbox
  val box_apply2 :
    ('-> '-> 'c) ->
    'Bindlib.bindbox -> 'Bindlib.bindbox -> 'Bindlib.bindbox
  val bind :
    ('Bindlib.var -> 'a) ->
    string ->
    ('Bindlib.bindbox -> 'Bindlib.bindbox) ->
    ('a, 'b) Bindlib.binder Bindlib.bindbox
  val mbind :
    ('Bindlib.var -> 'a) ->
    string array ->
    ('Bindlib.bindbox array -> 'Bindlib.bindbox) ->
    ('a, 'b) Bindlib.mbinder Bindlib.bindbox
  val unbox : 'Bindlib.bindbox -> 'a
  val vbind :
    ('Bindlib.var -> 'a) ->
    string ->
    ('Bindlib.var -> 'Bindlib.bindbox) ->
    ('a, 'b) Bindlib.binder Bindlib.bindbox
  val mvbind :
    ('Bindlib.var -> 'a) ->
    string array ->
    ('Bindlib.var array -> 'Bindlib.bindbox) ->
    ('a, 'b) Bindlib.mbinder Bindlib.bindbox
  val bind_var :
    'Bindlib.var ->
    'Bindlib.bindbox -> ('a, 'b) Bindlib.binder Bindlib.bindbox
  val bind_mvar :
    'Bindlib.mvar ->
    'Bindlib.bindbox -> ('a, 'b) Bindlib.mbinder Bindlib.bindbox
  val box_opt : 'Bindlib.bindbox option -> 'a option Bindlib.bindbox
  val box_list : 'Bindlib.bindbox list -> 'a list Bindlib.bindbox
  val box_rev_list : 'Bindlib.bindbox list -> 'a list Bindlib.bindbox
  val box_array : 'Bindlib.bindbox array -> 'a array Bindlib.bindbox
  val box_apply3 :
    ('-> '-> '-> 'd) ->
    'Bindlib.bindbox ->
    'Bindlib.bindbox -> 'Bindlib.bindbox -> 'Bindlib.bindbox
  val box_apply4 :
    ('-> '-> '-> '-> 'e) ->
    'Bindlib.bindbox ->
    'Bindlib.bindbox ->
    'Bindlib.bindbox -> 'Bindlib.bindbox -> 'Bindlib.bindbox
  val box_pair :
    'Bindlib.bindbox -> 'Bindlib.bindbox -> ('a * 'b) Bindlib.bindbox
  val box_triple :
    'Bindlib.bindbox ->
    'Bindlib.bindbox ->
    'Bindlib.bindbox -> ('a * 'b * 'c) Bindlib.bindbox
  module type Map =
    sig
      type 'a t
      val map : ('-> 'b) -> 'Bindlib.Map.t -> 'Bindlib.Map.t
    end
  module Lift :
    functor (M : Map->
      sig val lift_box : 'Bindlib.bindbox M.t -> 'M.t Bindlib.bindbox end
  module type Map2 =
    sig
      type ('a, 'b) t
      val map :
        ('-> 'b) ->
        ('-> 'd) -> ('a, 'c) Bindlib.Map2.t -> ('b, 'd) Bindlib.Map2.t
    end
  module Lift2 :
    functor (M : Map2->
      sig
        val lift_box :
          ('Bindlib.bindbox, 'Bindlib.bindbox) M.t ->
          ('a, 'b) M.t Bindlib.bindbox
      end
  val prefix_of : 'Bindlib.var -> string
  val suffix_of : 'Bindlib.var -> int
  val hash_var : 'Bindlib.var -> int
  val compare_vars : 'Bindlib.var -> 'Bindlib.var -> int
  val eq_vars : 'Bindlib.var -> 'Bindlib.var -> bool
  val copy_var :
    'Bindlib.var -> string -> ('Bindlib.var -> 'a) -> 'Bindlib.var
  val binder_name : ('a, 'b) Bindlib.binder -> string
  val binder_occur : ('a, 'b) Bindlib.binder -> bool
  val binder_constant : ('a, 'b) Bindlib.binder -> bool
  val binder_closed : ('a, 'b) Bindlib.binder -> bool
  val binder_rank : ('a, 'b) Bindlib.binder -> int
  val binder_compose_left :
    ('-> 'b) -> ('b, 'c) Bindlib.binder -> ('a, 'c) Bindlib.binder
  val binder_compose_right :
    ('a, 'b) Bindlib.binder -> ('-> 'c) -> ('a, 'c) Bindlib.binder
  val mbinder_arity : ('a, 'b) Bindlib.mbinder -> int
  val mbinder_names : ('a, 'b) Bindlib.mbinder -> string array
  val mbinder_occurs : ('a, 'b) Bindlib.mbinder -> bool array
  val mbinder_constant : ('a, 'b) Bindlib.mbinder -> bool
  val mbinder_closed : ('a, 'b) Bindlib.mbinder -> bool
  val mbinder_rank : ('a, 'b) Bindlib.mbinder -> int
  val is_closed : 'Bindlib.bindbox -> bool
  val is_substituted : (bool -> 'a) Bindlib.bindbox -> 'Bindlib.bindbox
  val occur : 'Bindlib.var -> 'Bindlib.bindbox -> bool
  val bind_apply :
    ('a, 'b) Bindlib.binder Bindlib.bindbox ->
    'Bindlib.bindbox -> 'Bindlib.bindbox
  val mbind_apply :
    ('a, 'b) Bindlib.mbinder Bindlib.bindbox ->
    'a array Bindlib.bindbox -> 'Bindlib.bindbox
  val fixpoint :
    (('a, 'b) Bindlib.binder, ('a, 'b) Bindlib.binder) Bindlib.binder
    Bindlib.bindbox -> ('a, 'b) Bindlib.binder Bindlib.bindbox
  type ctxt
  val empty_ctxt : Bindlib.ctxt
  val new_var_in :
    Bindlib.ctxt ->
    ('Bindlib.var -> 'a) -> string -> 'Bindlib.var * Bindlib.ctxt
  val new_mvar_in :
    Bindlib.ctxt ->
    ('Bindlib.var -> 'a) -> string array -> 'Bindlib.mvar * Bindlib.ctxt
  val unbind_in :
    Bindlib.ctxt ->
    ('Bindlib.var -> 'a) ->
    ('a, 'b) Bindlib.binder -> 'Bindlib.var * 'b * Bindlib.ctxt
  val unmbind_in :
    Bindlib.ctxt ->
    ('Bindlib.var -> 'a) ->
    ('a, 'b) Bindlib.mbinder -> 'Bindlib.mvar * 'b * Bindlib.ctxt
  val bind_in :
    Bindlib.ctxt ->
    ('Bindlib.var -> 'a) ->
    string ->
    ('Bindlib.bindbox -> Bindlib.ctxt -> 'Bindlib.bindbox) ->
    ('a, 'b) Bindlib.binder Bindlib.bindbox
  val mbind_in :
    Bindlib.ctxt ->
    ('Bindlib.var -> 'a) ->
    string array ->
    ('Bindlib.bindbox array -> Bindlib.ctxt -> 'Bindlib.bindbox) ->
    ('a, 'b) Bindlib.mbinder Bindlib.bindbox
  val reset_counter : unit -> unit
  val dummy_bindbox : 'Bindlib.bindbox
  val binder_from_fun : string -> ('-> 'b) -> ('a, 'b) Bindlib.binder
  val mbinder_from_fun :
    string array -> ('a array -> 'b) -> ('a, 'b) Bindlib.mbinder
end