sig
  type variable
  and symbol
  and compound
  and term =
      Variable of Term.variable
    | Constant of Term.symbol
    | Compound of Term.compound
    | Integer of int
    | Float of float
    | Unbound
  val make_variable : int -> Term.variable
  val variable_number : Term.variable -> int
  val gensym : unit -> Term.symbol
  val symbol_name : Term.symbol -> string
  val symbol_arity : Term.symbol -> int
  val make_compound : Term.symbol -> Term.term array -> Term.compound
  val compound_functor : Term.compound -> Term.symbol
  val compound_args : Term.compound -> Term.term array
  type symbol_table
  val make_symbol_table : unit -> Term.symbol_table
  val find_symbol : Term.symbol_table -> string -> int -> Term.symbol
  val symbol_table_iter : (Term.symbol -> unit) -> Term.symbol_table -> unit
  val get_meta_functor_symbol : Term.symbol_table -> Term.symbol
  val get_rule_symbol : Term.symbol_table -> Term.symbol
  val get_disjunction_symbol : Term.symbol_table -> Term.symbol
  val get_conjunction_symbol : Term.symbol_table -> Term.symbol
  val get_true_symbol : Term.symbol_table -> Term.symbol
  val get_false_symbol : Term.symbol_table -> Term.symbol
  val get_stratified_neg_as_failure_symbol : Term.symbol_table -> Term.symbol
  val get_stratified_neg_as_failure_alternate_symbol :
    Term.symbol_table -> Term.symbol
  val get_stratified_neg_as_failure_not_subsumed_symbol :
    Term.symbol_table -> Term.symbol
  val get_findall_symbol : Term.symbol_table -> Term.symbol
  val get_neg2_symbol : Term.symbol_table -> Term.symbol
  val set_meta_functor_symbol : Term.symbol_table -> Term.symbol -> unit
  val set_rule_symbol : Term.symbol_table -> Term.symbol -> unit
  val set_disjunction_symbol : Term.symbol_table -> Term.symbol -> unit
  val set_conjunction_symbol : Term.symbol_table -> Term.symbol -> unit
  val set_true_symbol : Term.symbol_table -> Term.symbol -> unit
  val set_false_symbol : Term.symbol_table -> Term.symbol -> unit
  val set_stratified_neg_as_failure_symbol :
    Term.symbol_table -> Term.symbol -> unit
  val set_stratified_neg_as_failure_alternate_symbol :
    Term.symbol_table -> Term.symbol -> unit
  val set_stratified_neg_as_failure_not_subsumed_symbol :
    Term.symbol_table -> Term.symbol -> unit
  val set_findall_symbol : Term.symbol_table -> Term.symbol -> unit
  val set_neg2_symbol : Term.symbol_table -> Term.symbol -> unit
  type context
  val max_vars : int
  exception Max_vars_exceeded
  val make_context : int -> Term.context
  val null_context : Term.context
  val context_multiplier : Term.context -> int
  val dereference : Term.term -> Term.context -> Term.term * Term.context
  type trail
  val make_trail : unit -> Term.trail
  val fail : Term.trail
  val failed : Term.trail -> bool
  type saved_trail
  val save_trail : Term.trail -> Term.saved_trail
  val undo_bindings : Term.trail -> Term.saved_trail -> Term.trail
  val unify :
    Term.term ->
    Term.context -> Term.term -> Term.context -> Term.trail -> Term.trail
  val apply : Term.term -> Term.context -> Term.term
  val copy_term : Term.term -> Term.term
  val match_terms :
    Term.term -> Term.context -> Term.term -> Term.trail -> Term.trail
  val subsumes_chk : Term.term -> Term.term -> bool
  val variant : Term.term -> Term.term -> bool
  val term_ident : Term.term -> Term.term -> bool
  val renumber_variables_term : int array -> Term.term -> unit
  type deterministic_builtin =
    Term.term -> Term.context -> Term.context -> Term.trail -> Term.trail
  type p =
      PUnbound
    | PDeterministic of Term.deterministic_builtin *
        (Opt.mode_specifier * Opt.discrimination_values * Opt.proof)
  val symbol_predicate : Term.symbol -> Term.p
  val set_symbol_predicate : Term.symbol -> Term.p -> unit
  type f =
      FUnbound
    | FUnary of (Term.term -> Term.term)
    | FBinary of (Term.term -> Term.term -> Term.term)
  val symbol_function : Term.symbol -> Term.f
  val set_symbol_function : Term.symbol -> Term.f -> unit
end