sig
  type oracle_quant_var =
      Why3.Pinterp_core.env ->
      Why3.Term.vsymbol -> Why3.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 ->
    Why3.Pinterp_core.oracle -> Rac.oracle_quant_var
  module Why :
    sig
      type why_prover = {
        command : string;
        driver : Why3.Driver.driver;
        limits : Why3.Call_provers.resource_limits;
      }
      val mk_why_prover :
        command:string ->
        Why3.Driver.driver ->
        Why3.Call_provers.resource_limits -> Rac.Why.why_prover
      val mk_check_term :
        ?metas:(Why3.Theory.meta * Why3.Theory.meta_arg list) list ->
        ?trans:Why3.Task.task Why3.Trans.tlist ->
        ?why_prover:Rac.Why.why_prover ->
        ?oracle_quant_var:Rac.oracle_quant_var ->
        config:Why3.Whyconf.config ->
        elim_eps:Why3.Task.task Why3.Trans.trans ->
        unit -> Why3.Pinterp_core.check_term
      val mk_check_term_lit :
        Why3.Whyconf.config ->
        Why3.Env.env ->
        ?metas:(string * string option) list ->
        ?trans:string ->
        why_prover:(string * Why3.Call_provers.resource_limits) option ->
        ?oracle_quant_var:Rac.oracle_quant_var ->
        unit -> Why3.Pinterp_core.check_term
      val mk_compute_term :
        ?metas:(Why3.Theory.meta * Why3.Theory.meta_arg list) list ->
        ?trans:Why3.Task.task list Why3.Trans.trans ->
        ?oracle_quant_var:Rac.oracle_quant_var ->
        unit -> Why3.Pinterp_core.compute_term
      val mk_compute_term_lit :
        Why3.Env.env ->
        ?metas:(string * string option) list ->
        ?trans:string ->
        ?oracle_quant_var:Rac.oracle_quant_var ->
        unit -> Why3.Pinterp_core.compute_term
    end
end