sig
  val tprinter : Why3.Ident.ident_printer
  val aprinter : Why3.Ident.ident_printer
  val sprinter : Why3.Ident.ident_printer
  val pprinter : Why3.Ident.ident_printer
  val forget_all : unit -> unit
  val forget_tvs : unit -> unit
  val forget_var : Why3.Term.vsymbol -> unit
  val print_id_attrs : Why3.Ident.ident Why3.Pp.pp
  val print_tv : Why3.Ty.tvsymbol Why3.Pp.pp
  val print_vs : Why3.Term.vsymbol Why3.Pp.pp
  val print_ts : Why3.Ty.tysymbol Why3.Pp.pp
  val print_ls : Why3.Term.lsymbol Why3.Pp.pp
  val print_cs : Why3.Term.lsymbol Why3.Pp.pp
  val print_pr : Why3.Decl.prsymbol Why3.Pp.pp
  val print_th : Why3.Theory.theory Why3.Pp.pp
  val print_ty : Why3.Ty.ty Why3.Pp.pp
  val print_vsty : Why3.Term.vsymbol Why3.Pp.pp
  val print_ts_qualified : Why3.Ty.tysymbol Why3.Pp.pp
  val print_ls_qualified : Why3.Term.lsymbol Why3.Pp.pp
  val print_cs_qualified : Why3.Term.lsymbol Why3.Pp.pp
  val print_pr_qualified : Why3.Decl.prsymbol Why3.Pp.pp
  val print_th_qualified : Why3.Theory.theory Why3.Pp.pp
  val print_ty_qualified : Why3.Ty.ty Why3.Pp.pp
  val print_vs_qualified : Why3.Term.vsymbol Why3.Pp.pp
  val print_tv_qualified : Why3.Ty.tvsymbol Why3.Pp.pp
  val print_quant : Why3.Term.quant Why3.Pp.pp
  val print_binop : asym:bool -> Why3.Term.binop Why3.Pp.pp
  val print_pat : Why3.Term.pattern Why3.Pp.pp
  val print_term : Why3.Term.term Why3.Pp.pp
  val print_attr : Why3.Ident.attribute Why3.Pp.pp
  val print_attrs : Why3.Ident.Sattr.t Why3.Pp.pp
  val print_loc_as_attribute : Why3.Loc.position Why3.Pp.pp
  val print_pkind : Why3.Decl.prop_kind Why3.Pp.pp
  val print_meta_arg : Why3.Theory.meta_arg Why3.Pp.pp
  val print_meta_arg_type : Why3.Theory.meta_arg_type Why3.Pp.pp
  val print_ty_decl : Why3.Ty.tysymbol Why3.Pp.pp
  val print_data_decl : Why3.Decl.data_decl Why3.Pp.pp
  val print_param_decl : Why3.Term.lsymbol Why3.Pp.pp
  val print_logic_decl : Why3.Decl.logic_decl Why3.Pp.pp
  val print_ind_decl : Why3.Decl.ind_sign -> Why3.Decl.ind_decl Why3.Pp.pp
  val print_next_data_decl : Why3.Decl.data_decl Why3.Pp.pp
  val print_next_logic_decl : Why3.Decl.logic_decl Why3.Pp.pp
  val print_next_ind_decl : Why3.Decl.ind_decl Why3.Pp.pp
  val print_prop_decl : Why3.Decl.prop_decl Why3.Pp.pp
  val print_decl : Why3.Decl.decl Why3.Pp.pp
  val print_tdecl : Why3.Theory.tdecl Why3.Pp.pp
  val print_task : Why3.Task.task Why3.Pp.pp
  val print_sequent : Why3.Task.task Why3.Pp.pp
  val print_theory : Why3.Theory.theory Why3.Pp.pp
  val print_namespace : string -> Why3.Theory.theory Why3.Pp.pp
end