sig
  type term =
      Term of string * Term.term array * Term.term array
    | SVar of string * int * Term.term * Term.term array
    | TVar of string * Term.term option
  val fun_type_name : string
  val assign_name : string
  val symbol_of_term : Term.term -> string
  val term_str : Term.term -> string
  val short_term : (Term.term -> string) Pervasives.ref
  val suffix : int -> Term.term -> Term.term
  val equal_mod_tvars : Term.term -> Term.term -> bool
  val size_up_to : int -> Term.term -> int
  val s_vars_in_term : string list -> Term.term -> string list
  val t_vars_in_term : string list -> Term.term -> string list
  val has_s_var : Term.term -> bool
  val has_t_var : Term.term -> bool
  val fn_apply : int -> ('a -> 'a) -> 'a -> 'a
  val add_logic_name : string -> unit
  type t_subst
  type s_subst
  type substs = Term.s_subst * Term.t_subst
  exception UNIFY
  val empty_s_sb : Term.s_subst
  val empty_t_sb : Term.t_subst
  val empty_sbs : Term.substs
  val assoc_t_sb : string -> Term.t_subst -> Term.term
  val assoc_s_sb : string -> Term.s_subst -> Term.term
  val apply_sbs : Term.substs -> Term.term -> Term.term
  val head_grounding : Term.term -> Term.term
  val types_of : Term.term -> Term.term array
  type position
  val position_str : Term.position -> string
  val subst_t_pos : Term.position -> subt:Term.term -> Term.term -> Term.term
  val get_t_pos : Term.position -> Term.term -> Term.term
  type iter_s_subst
  type iter_t_subst
  type isubsts = Term.iter_s_subst * Term.iter_t_subst
  val empty_t_isb : Term.iter_t_subst
  val empty_s_isb : Term.iter_s_subst
  val empty_isbs : Term.isubsts
  type add_to_decls =
      Decls_OK
    | Decls_multi_glb of string * string * string
    | Decls_multi_lub of string * string * string
    | Decls_redundant_s of string * string
    | Decls_polyconflict
    | Decls_var
    | Decls_repeating of string
  type decls_set
  val create_decls : unit -> Term.decls_set
  val get_superclasses : Term.decls_set -> string -> Aux.Strings.t
  val get_subclasses : Term.decls_set -> string -> string list
  val get_decl : Term.decls_set -> string -> Term.term
  exception EXC_Decls_multi_lub of string * string * string
  val add_to_decls : Term.decls_set -> Term.term -> Term.add_to_decls
  val glb :
    Term.decls_set -> Term.term -> Term.term -> Term.isubsts * Term.term
  val aux_glb :
    Term.decls_set ->
    Term.isubsts -> Term.term -> Term.term -> Term.isubsts * Term.term
  val lub :
    Term.decls_set -> Term.term -> Term.term -> Term.isubsts * Term.term
  val aux_lub :
    Term.decls_set ->
    Term.isubsts -> Term.term -> Term.term -> Term.isubsts * Term.term
  val aux_glb_lub_cont :
    Term.decls_set -> Term.isubsts -> Term.isubsts -> Term.isubsts
  val isa_match :
    Term.decls_set ->
    ?for_rewrite:bool ->
    pattern:Term.term -> Term.term -> Term.substs * Term.position
  val equal_for_rewriting : Term.decls_set -> Term.term -> Term.term -> bool
  val isa_unify :
    Term.decls_set -> pattern:Term.term -> Term.term -> Term.isubsts
  val aux_isa_unify :
    Term.decls_set ->
    Term.isubsts -> pattern:Term.term -> Term.term -> Term.isubsts
  val is_superclass_of :
    Term.decls_set -> pattern:Term.term -> Term.term -> bool
  val mgu_iter : Term.decls_set -> Term.term -> Term.term -> Term.isubsts
  val aux_mgu_i :
    Term.decls_set -> Term.isubsts -> Term.term -> Term.term -> Term.isubsts
  val aux_mgu_i_cont :
    Term.decls_set -> Term.isubsts -> Term.isubsts -> Term.isubsts
  val apply_isbs : Term.isubsts -> Term.term -> Term.term
  val split_to_list : string -> Aux.split_result list
  val s_subst_str : Term.s_subst -> string
  val t_subst_str : Term.t_subst -> string
  val t_isubst_str : Term.iter_t_subst -> string
  val substs_str : Term.substs -> string
  val substs_fstr : (Term.term -> string) -> Term.substs -> string
  val isubsts_str : Term.isubsts -> string
  val isubsts_fstr : (Term.term -> string) -> Term.isubsts -> string
  val t_isubst_map :
    (Term.term -> Term.term) -> Term.iter_t_subst -> Term.iter_t_subst
  val s_isubst_map_some :
    (string * (int * Term.term) -> (string * (int * Term.term)) option) ->
    Term.iter_s_subst -> Term.iter_s_subst
  val isubsts_map : (Term.term -> Term.term) -> Term.isubsts -> Term.isubsts
  module HashableTerm :
    sig
      type t = Term.term
      val equal : Term.HashableTerm.t -> Term.HashableTerm.t -> bool
      val hash : Term.HashableTerm.t -> int
    end
  module TermHashtbl :
    sig
      type key = Term.HashableTerm.t
      type 'a t = 'a Hashtbl.Make(HashableTerm).t
      val create : int -> 'a Term.TermHashtbl.t
      val clear : 'a Term.TermHashtbl.t -> unit
      val copy : 'a Term.TermHashtbl.t -> 'a Term.TermHashtbl.t
      val add : 'a Term.TermHashtbl.t -> Term.TermHashtbl.key -> 'a -> unit
      val remove : 'a Term.TermHashtbl.t -> Term.TermHashtbl.key -> unit
      val find : 'a Term.TermHashtbl.t -> Term.TermHashtbl.key -> 'a
      val find_all : 'a Term.TermHashtbl.t -> Term.TermHashtbl.key -> 'a list
      val replace :
        'a Term.TermHashtbl.t -> Term.TermHashtbl.key -> 'a -> unit
      val mem : 'a Term.TermHashtbl.t -> Term.TermHashtbl.key -> bool
      val iter :
        (Term.TermHashtbl.key -> 'a -> unit) -> 'a Term.TermHashtbl.t -> unit
      val fold :
        (Term.TermHashtbl.key -> 'a -> 'b -> 'b) ->
        'a Term.TermHashtbl.t -> 'b -> 'b
      val length : 'a Term.TermHashtbl.t -> int
    end
end