sig
  type scope = Qed.Engine.scope
  module Env :
    sig
      type t
      val create : unit -> t
      val copy : t -> t
      val clear : t -> unit
      val used : t -> string -> bool
      val fresh : t -> ?suggest:bool -> string -> string
      val define : t -> string -> Lang.F.term -> unit
      val unfold : t -> Lang.F.term -> unit
      val shared : t -> Lang.F.term -> bool
      val shareable : t -> Lang.F.term -> bool
      val force_index : t -> unit
    end
  type pool
  val pool : unit -> Plang.pool
  val alloc_e : Plang.pool -> (Lang.F.var -> unit) -> Lang.F.term -> unit
  val alloc_p : Plang.pool -> (Lang.F.var -> unit) -> Lang.F.pred -> unit
  val alloc_xs : Plang.pool -> (Lang.F.var -> unit) -> Lang.F.Vars.t -> unit
  val alloc_domain : Plang.pool -> Lang.F.Vars.t
  class engine :
    object
      method basename : string -> string
      method bind : Lang.F.var -> string
      method callstyle : Qed.Engine.callstyle
      method datatype : Lang.ADT.t -> string
      method datatypename : string -> string
      method e_false : Qed.Engine.cmode -> string
      method e_true : Qed.Engine.cmode -> string
      method env : Env.t
      method field : Lang.Field.t -> string
      method fieldname : string -> string
      method find : Lang.F.var -> string
      method funname : string -> string
      method global : (unit -> unit) -> unit
      method infoprover : 'Lang.infoprover -> 'a
      method is_atomic : Lang.F.term -> bool
      method link : Lang.Fun.t -> Qed.Engine.link
      method local : (unit -> unit) -> unit
      method lookup : Lang.F.term -> Qed.Engine.scope
      method marks : Plang.Env.t * Lang.F.marks
      method mode : Qed.Engine.mode
      method op_add : Qed.Engine.amode -> Qed.Engine.op
      method op_and : Qed.Engine.cmode -> Qed.Engine.op
      method op_div : Qed.Engine.amode -> Qed.Engine.op
      method op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
      method op_equal : Qed.Engine.cmode -> Qed.Engine.op
      method op_equiv : Qed.Engine.cmode -> Qed.Engine.op
      method op_imply : Qed.Engine.cmode -> Qed.Engine.op
      method op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
      method op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
      method op_minus : Qed.Engine.amode -> Qed.Engine.op
      method op_mod : Qed.Engine.amode -> Qed.Engine.op
      method op_mul : Qed.Engine.amode -> Qed.Engine.op
      method op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
      method op_not : Qed.Engine.cmode -> Qed.Engine.op
      method op_noteq : Qed.Engine.cmode -> Qed.Engine.op
      method op_or : Qed.Engine.cmode -> Qed.Engine.op
      method op_real_of_int : Qed.Engine.op
      method op_scope : Qed.Engine.amode -> string option
      method op_spaced : string -> bool
      method op_sub : Qed.Engine.amode -> Qed.Engine.op
      method pp_apply :
        Qed.Engine.cmode -> Lang.F.term -> Lang.F.term list Qed.Plib.printer
      method pp_array : Lang.F.tau Qed.Plib.printer
      method pp_array_get :
        Format.formatter -> Lang.F.term -> Lang.F.term -> unit
      method pp_array_set :
        Format.formatter -> Lang.F.term -> Lang.F.term -> Lang.F.term -> unit
      method pp_atom : Lang.F.term Qed.Plib.printer
      method pp_conditional :
        Format.formatter -> Lang.F.term -> Lang.F.term -> Lang.F.term -> unit
      method pp_datatype : Lang.ADT.t -> Lang.F.tau list Qed.Plib.printer
      method pp_def_fields :
        (Lang.Field.t * Lang.F.term) list Qed.Plib.printer
      method pp_equal : Lang.F.term Qed.Plib.printer2
      method pp_exists : Lang.F.tau -> string list Qed.Plib.printer
      method pp_expr : Lang.F.tau -> Lang.F.term Qed.Plib.printer
      method pp_farray : Lang.F.tau Qed.Plib.printer2
      method pp_flow : Lang.F.term Qed.Plib.printer
      method pp_forall : Lang.F.tau -> string list Qed.Plib.printer
      method pp_fun :
        Qed.Engine.cmode -> Lang.Fun.t -> Lang.F.term list Qed.Plib.printer
      method pp_get_field :
        Format.formatter -> Lang.F.term -> Lang.Field.t -> unit
      method pp_imply :
        Format.formatter -> Lang.F.term list -> Lang.F.term -> unit
      method pp_int : Qed.Engine.amode -> Z.t Qed.Plib.printer
      method pp_lambda : (string * Lang.F.tau) list Qed.Plib.printer
      method pp_let :
        Format.formatter -> Qed.Engine.pmode -> string -> Lang.F.term -> unit
      method pp_not : Lang.F.term Qed.Plib.printer
      method pp_noteq : Lang.F.term Qed.Plib.printer2
      method pp_pred : Format.formatter -> Lang.F.pred -> unit
      method pp_prop : Lang.F.term Qed.Plib.printer
      method pp_real : Q.t Qed.Plib.printer
      method pp_repr : Lang.F.term Qed.Plib.printer
      method pp_sort : Lang.F.term Qed.Plib.printer
      method pp_subtau : Lang.F.tau Qed.Plib.printer
      method pp_tau : Lang.F.tau Qed.Plib.printer
      method pp_term : Lang.F.term Qed.Plib.printer
      method pp_times : Format.formatter -> Z.t -> Lang.F.term -> unit
      method pp_tvar : int Qed.Plib.printer
      method pp_var : string Qed.Plib.printer
      method scope : Env.t -> (unit -> unit) -> unit
      method set_env : Env.t -> unit
      method shareable : Lang.F.term -> bool
      method shared : Lang.F.term -> bool
      method subterms : (Lang.F.term -> unit) -> Lang.F.term -> unit
      method t_atomic : Lang.F.tau -> bool
      method t_bool : string
      method t_int : string
      method t_prop : string
      method t_real : string
      method with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit
    end
end