sig
  val coercion_attr : Why3.Ident.attribute
  val why3_keywords : string list
  val prio_binop : Why3.Term.binop -> int
  val protect_on :
    bool ->
    ('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6 ->
    ('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6
  type syntax = Is_array of string | Is_getter of string | Is_none
  val get_element_syntax : attrs:Why3.Ident.Sattr.t -> Pretty.syntax
  module type Printer =
    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
  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
  type any_pp =
      Pp_term of (Why3.Term.term * int)
    | Pp_ty of (Why3.Ty.ty * int * bool)
    | Pp_decl of
        (bool * Why3.Ty.tysymbol *
         (Why3.Term.lsymbol * Why3.Term.lsymbol option list) list)
    | Pp_ts of Why3.Ty.tysymbol
    | Pp_ls of Why3.Term.lsymbol
    | Pp_id of Why3.Ident.ident
    | Pp_cs of Why3.Term.lsymbol
    | Pp_vs of Why3.Term.vsymbol
    | Pp_trigger of Why3.Term.trigger
    | Pp_forget of Why3.Term.vsymbol list
    | Pp_forget_tvs
  val create :
    ?print_ext_any:(Pretty.any_pp Why3.Pp.pp -> Pretty.any_pp Why3.Pp.pp) ->
    ?do_forget_all:bool ->
    ?shorten_axioms:bool ->
    ?show_uses_clones_metas:bool ->
    Why3.Ident.ident_printer ->
    Why3.Ident.ident_printer ->
    Why3.Ident.ident_printer ->
    Why3.Ident.ident_printer -> (module Pretty.Printer)
end