sig
  val coercion_attr : Ident.attribute
  val why3_keywords : string list
  val prio_binop : 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:Ident.Sattr.t -> Pretty.syntax
  module type Printer =
    sig
      val tprinter : Ident.ident_printer
      val aprinter : Ident.ident_printer
      val sprinter : Ident.ident_printer
      val pprinter : Ident.ident_printer
      val forget_all : unit -> unit
      val forget_tvs : unit -> unit
      val forget_var : Term.vsymbol -> unit
      val print_id_attrs : Ident.ident Pp.pp
      val print_tv : Ty.tvsymbol Pp.pp
      val print_vs : Term.vsymbol Pp.pp
      val print_ts : Ty.tysymbol Pp.pp
      val print_ls : Term.lsymbol Pp.pp
      val print_cs : Term.lsymbol Pp.pp
      val print_pr : Decl.prsymbol Pp.pp
      val print_th : Theory.theory Pp.pp
      val print_ty : Ty.ty Pp.pp
      val print_vsty : Term.vsymbol Pp.pp
      val print_ts_qualified : Ty.tysymbol Pp.pp
      val print_ls_qualified : Term.lsymbol Pp.pp
      val print_cs_qualified : Term.lsymbol Pp.pp
      val print_pr_qualified : Decl.prsymbol Pp.pp
      val print_th_qualified : Theory.theory Pp.pp
      val print_ty_qualified : Ty.ty Pp.pp
      val print_vs_qualified : Term.vsymbol Pp.pp
      val print_tv_qualified : Ty.tvsymbol Pp.pp
      val print_quant : Term.quant Pp.pp
      val print_binop : asym:bool -> Term.binop Pp.pp
      val print_pat : Term.pattern Pp.pp
      val print_term : Term.term Pp.pp
      val print_attr : Ident.attribute Pp.pp
      val print_attrs : Ident.Sattr.t Pp.pp
      val print_loc_as_attribute : Loc.position Pp.pp
      val print_pkind : Decl.prop_kind Pp.pp
      val print_meta_arg : Theory.meta_arg Pp.pp
      val print_meta_arg_type : Theory.meta_arg_type Pp.pp
      val print_ty_decl : Ty.tysymbol Pp.pp
      val print_data_decl : Decl.data_decl Pp.pp
      val print_param_decl : Term.lsymbol Pp.pp
      val print_logic_decl : Decl.logic_decl Pp.pp
      val print_ind_decl : Decl.ind_sign -> Decl.ind_decl Pp.pp
      val print_next_data_decl : Decl.data_decl Pp.pp
      val print_next_logic_decl : Decl.logic_decl Pp.pp
      val print_next_ind_decl : Decl.ind_decl Pp.pp
      val print_prop_decl : Decl.prop_decl Pp.pp
      val print_decl : Decl.decl Pp.pp
      val print_tdecl : Theory.tdecl Pp.pp
      val print_task : Task.task Pp.pp
      val print_sequent : Task.task Pp.pp
      val print_theory : Theory.theory Pp.pp
      val print_namespace : string -> Theory.theory Pp.pp
    end
  val tprinter : Ident.ident_printer
  val aprinter : Ident.ident_printer
  val sprinter : Ident.ident_printer
  val pprinter : Ident.ident_printer
  val forget_all : unit -> unit
  val forget_tvs : unit -> unit
  val forget_var : Term.vsymbol -> unit
  val print_id_attrs : Ident.ident Pp.pp
  val print_tv : Ty.tvsymbol Pp.pp
  val print_vs : Term.vsymbol Pp.pp
  val print_ts : Ty.tysymbol Pp.pp
  val print_ls : Term.lsymbol Pp.pp
  val print_cs : Term.lsymbol Pp.pp
  val print_pr : Decl.prsymbol Pp.pp
  val print_th : Theory.theory Pp.pp
  val print_ty : Ty.ty Pp.pp
  val print_vsty : Term.vsymbol Pp.pp
  val print_ts_qualified : Ty.tysymbol Pp.pp
  val print_ls_qualified : Term.lsymbol Pp.pp
  val print_cs_qualified : Term.lsymbol Pp.pp
  val print_pr_qualified : Decl.prsymbol Pp.pp
  val print_th_qualified : Theory.theory Pp.pp
  val print_ty_qualified : Ty.ty Pp.pp
  val print_vs_qualified : Term.vsymbol Pp.pp
  val print_tv_qualified : Ty.tvsymbol Pp.pp
  val print_quant : Term.quant Pp.pp
  val print_binop : asym:bool -> Term.binop Pp.pp
  val print_pat : Term.pattern Pp.pp
  val print_term : Term.term Pp.pp
  val print_attr : Ident.attribute Pp.pp
  val print_attrs : Ident.Sattr.t Pp.pp
  val print_loc_as_attribute : Loc.position Pp.pp
  val print_pkind : Decl.prop_kind Pp.pp
  val print_meta_arg : Theory.meta_arg Pp.pp
  val print_meta_arg_type : Theory.meta_arg_type Pp.pp
  val print_ty_decl : Ty.tysymbol Pp.pp
  val print_data_decl : Decl.data_decl Pp.pp
  val print_param_decl : Term.lsymbol Pp.pp
  val print_logic_decl : Decl.logic_decl Pp.pp
  val print_ind_decl : Decl.ind_sign -> Decl.ind_decl Pp.pp
  val print_next_data_decl : Decl.data_decl Pp.pp
  val print_next_logic_decl : Decl.logic_decl Pp.pp
  val print_next_ind_decl : Decl.ind_decl Pp.pp
  val print_prop_decl : Decl.prop_decl Pp.pp
  val print_decl : Decl.decl Pp.pp
  val print_tdecl : Theory.tdecl Pp.pp
  val print_task : Task.task Pp.pp
  val print_sequent : Task.task Pp.pp
  val print_theory : Theory.theory Pp.pp
  val print_namespace : string -> Theory.theory Pp.pp
  type any_pp =
      Pp_term of (Term.term * int)
    | Pp_ty of (Ty.ty * int * bool)
    | Pp_decl of
        (bool * Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list)
    | Pp_ts of Ty.tysymbol
    | Pp_ls of Term.lsymbol
    | Pp_id of Ident.ident
    | Pp_cs of Term.lsymbol
    | Pp_vs of Term.vsymbol
    | Pp_trigger of Term.trigger
    | Pp_forget of Term.vsymbol list
    | Pp_forget_tvs
  val create :
    ?print_ext_any:(Pretty.any_pp Pp.pp -> Pretty.any_pp Pp.pp) ->
    ?do_forget_all:bool ->
    ?shorten_axioms:bool ->
    ?show_uses_clones_metas:bool ->
    Ident.ident_printer ->
    Ident.ident_printer ->
    Ident.ident_printer -> Ident.ident_printer -> (module Pretty.Printer)
end