sig
  type config = Config.config
  type state = State.state
  type context = Context.context
  type literal = Term.literal
  type clause = Term.clause
  type choice_point = State.choice_point
  type explanation = State.explanation
  type raw_context_unifier = Context_unifier.raw_context_unifier
  val backtrack :
    State_backtrack.state ->
    State_backtrack.context ->
    State_backtrack.config ->
    State_backtrack.raw_context_unifier ->
    State_backtrack.choice_point * State_backtrack.literal list *
    State_backtrack.clause option
  val backtrack_incomplete :
    State_backtrack.state -> State_backtrack.choice_point -> unit
end