sig
  type why_prover = {
    command : string;
    driver : Driver.driver;
    limit : Call_provers.resource_limit;
  }
  val mk_why_prover :
    command:string ->
    Driver.driver -> Call_provers.resource_limit -> Rac.Why.why_prover
  val mk_check_term :
    ?metas:(Theory.meta * Theory.meta_arg list) list ->
    ?trans:Task.task Trans.tlist ->
    ?why_prover:Rac.Why.why_prover ->
    ?oracle_quant_var:Rac.oracle_quant_var ->
    config:Whyconf.config ->
    elim_eps:Task.task Trans.trans -> unit -> Pinterp_core.check_term
  val mk_check_term_lit :
    Whyconf.config ->
    Env.env ->
    ?metas:(string * string option) list ->
    ?trans:string ->
    ?why_prover:string ->
    ?oracle_quant_var:Rac.oracle_quant_var -> unit -> Pinterp_core.check_term
  val mk_compute_term :
    ?metas:(Theory.meta * Theory.meta_arg list) list ->
    ?trans:Task.task list Trans.trans ->
    ?oracle_quant_var:Rac.oracle_quant_var ->
    unit -> Pinterp_core.compute_term
  val mk_compute_term_lit :
    Env.env ->
    ?metas:(string * string option) list ->
    ?trans:string ->
    ?oracle_quant_var:Rac.oracle_quant_var ->
    unit -> Pinterp_core.compute_term
end