sig
  type oracle_quant_var =
      Pinterp_core.env -> Term.vsymbol -> Pinterp_core.Value.value option
  val oracle_quant_var_dummy : Rac.oracle_quant_var
  val oracle_quant_var :
    ?bind_univ_quant_vars:bool ->
    ?bind_univ_quant_vars_default:bool ->
    Pinterp_core.oracle -> Rac.oracle_quant_var
  module Why :
    sig
      type why_prover = {
        command : string;
        driver : Driver.driver;
        limits : Call_provers.resource_limits;
      }
      val mk_why_prover :
        command:string ->
        Driver.driver -> Call_provers.resource_limits -> 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 * Call_provers.resource_limits) option ->
        ?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
end