object
  method bind : Lang.F.var -> string
  method callstyle : Qed.Engine.callstyle
  method clear : unit
  method datatype : Lang.ADT.t -> string
  method domain : Wp.Lang.F.Vars.t
  method e_false : Qed.Engine.cmode -> string
  method e_true : Qed.Engine.cmode -> string
  method env : Plang.Env.t
  method field : Lang.Field.t -> string
  method find : Lang.F.var -> string
  method global : (unit -> unit) -> unit
  method infoprover : 'Lang.infoprover -> 'a
  method is_atomic : Lang.F.term -> bool
  method is_atomic_lv : Sigs.s_lval -> bool
  method label_at : id:int -> Wp.Pcfg.label
  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_addr : Format.formatter -> Sigs.s_lval -> unit
  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_cst : Format.formatter -> Lang.F.tau -> Lang.F.term -> unit
  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_at : Format.formatter -> Wp.Pcfg.label -> unit
  method pp_atom : Lang.F.term Qed.Plib.printer
  method pp_chunk : Format.formatter -> string -> unit
  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_host : Format.formatter -> Sigs.s_host -> 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_label : Format.formatter -> Pcfg.label -> unit
  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_lval : Format.formatter -> Sigs.s_lval -> unit
  method pp_not : Lang.F.term Qed.Plib.printer
  method pp_noteq : Lang.F.term Qed.Plib.printer2
  method pp_offset : Format.formatter -> Sigs.s_offset list -> unit
  method pp_ofs : Format.formatter -> Sigs.s_offset -> unit
  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_update :
    Wp.Pcfg.label -> Format.formatter -> Wp.Sigs.update -> unit
  method pp_value : Format.formatter -> Wp.Lang.F.term -> unit
  method pp_var : string Qed.Plib.printer
  method sanitize : string -> string
  method sanitize_field : string -> string
  method sanitize_fun : string -> string
  method sanitize_type : string -> string
  method scope : Plang.Env.t -> (unit -> unit) -> unit
  method set_domain : Wp.Lang.F.Vars.t -> unit
  method set_env : Plang.Env.t -> unit
  method set_sequence : Wp.Conditions.sequence -> 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 updates : Wp.Pcfg.label Wp.Sigs.sequence -> Wp.Sigs.update Bag.t
  method with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit
end