sig
  type config = Config.config
  type bound = Bound.bound
  type statistic = Statistic.statistic
  type literal = Term.literal
  type subst = Subst.subst
  type choice_point = State.choice_point
  type state = State.state
  type context = Context.context
  type context_partner = Context_unifier.context_partner
  type input_partner = Context_unifier.input_partner
  type context_unifier_space = Context_unifier.context_unifier_space
  type problem_literals
  val create :
    Problem_literals.config ->
    Problem_literals.bound ->
    Problem_literals.statistic ->
    Problem_literals.state ->
    Problem_literals.context -> Problem_literals.problem_literals
  val register_literal :
    Problem_literals.problem_literals ->
    Problem_literals.literal -> int -> Problem_literals.input_partner
  val register_input_partner :
    Problem_literals.problem_literals ->
    Problem_literals.input_partner ->
    Problem_literals.context_unifier_space -> unit
  val unregister_space :
    Problem_literals.problem_literals ->
    Problem_literals.context_unifier_space -> unit
  val add :
    Problem_literals.problem_literals ->
    Context.element -> Context_unifier.candidate_type -> unit
  val compute_deferred :
    Problem_literals.problem_literals ->
    Context_unifier.candidate_type -> unit
  val compute_for_element :
    Problem_literals.problem_literals ->
    Context.element -> Context_unifier.candidate_type -> unit
  val is_space_subsumed :
    Problem_literals.problem_literals ->
    Problem_literals.context_unifier_space -> bool
  val backtrack : Problem_literals.problem_literals -> unit
end