sig
  val debug_parse_only : Why3.Debug.flag
  val debug_type_only : Why3.Debug.flag
  val warn_useless_at : Why3.Loc.warning_id
  val type_mlw_file :
    Why3.Env.env ->
    string list -> string -> Why3.Ptree.mlw_file -> Why3.Pmodule.mlw_file
  val open_file : Why3.Env.env -> Why3.Env.pathname -> unit
  val close_file : unit -> Why3.Pmodule.mlw_file
  val discard_file : unit -> unit
  val open_module : ?intf:Why3.Ptree.qualid -> Why3.Ptree.ident -> unit
  val close_module : Why3.Loc.position -> unit
  val open_scope : Why3.Loc.position -> Why3.Ptree.ident -> unit
  val close_scope : Why3.Loc.position -> import:bool -> unit
  val add_decl : Why3.Loc.position -> Why3.Ptree.decl -> unit
  val string_list_of_qualid : Why3.Ptree.qualid -> string list
  val print_qualid : Stdlib.Format.formatter -> Why3.Ptree.qualid -> unit
  val type_term_in_namespace :
    Why3.Theory.namespace ->
    Why3.Decl.known_map ->
    Why3.Coercion.t -> Why3.Ptree.term -> Why3.Term.term
  val type_fmla_in_namespace :
    Why3.Theory.namespace ->
    Why3.Decl.known_map ->
    Why3.Coercion.t -> Why3.Ptree.term -> Why3.Term.term
  val type_expr_in_muc :
    Why3.Pmodule.pmodule_uc ->
    ?denv:Why3.Dexpr.denv -> Why3.Ptree.expr -> Why3.Expr.expr
  module Unsafe :
    sig
      val dexpr :
        Why3.Pmodule.pmodule_uc ->
        Why3.Dexpr.denv -> Why3.Ptree.expr -> Why3.Dexpr.dexpr
      val drec_defn :
        Why3.Pmodule.pmodule_uc ->
        Why3.Dexpr.denv ->
        Why3.Ptree.fundef list -> Why3.Dexpr.denv * Why3.Dexpr.drec_defn
      val add_decl :
        Why3.Pmodule.pmodule_uc ->
        Why3.Env.env ->
        Why3.Pmodule.mlw_file -> Why3.Ptree.decl -> Why3.Pmodule.pmodule_uc
      val create_user_id : Why3.Ptree.ident -> Why3.Ident.preid
      val create_user_prog_id : Why3.Ptree.ident -> Why3.Ident.preid
    end
  val ty_of_pty : Why3.Theory.theory_uc -> Why3.Ptree.pty -> Why3.Ty.ty
  val type_term_in_denv :
    Why3.Theory.namespace ->
    Why3.Decl.known_map ->
    Why3.Coercion.t -> Why3.Dterm.denv -> Why3.Ptree.term -> Why3.Term.term
  val check_term_in_denv :
    Why3.Theory.namespace ->
    Why3.Decl.known_map ->
    Why3.Coercion.t ->
    Why3.Dterm.denv -> Why3.Ptree.term -> Why3.Ty.ty -> Why3.Term.term
  val type_fmla_in_denv :
    Why3.Theory.namespace ->
    Why3.Decl.known_map ->
    Why3.Coercion.t -> Why3.Dterm.denv -> Why3.Ptree.term -> Why3.Term.term
end