sig
  type prog_symbol =
      PV of Why3.Ity.pvsymbol
    | RS of Why3.Expr.rsymbol
    | OO of Why3.Expr.Srs.t
  type namespace = {
    ns_ts : Why3.Ity.itysymbol Why3.Wstdlib.Mstr.t;
    ns_ps : Pmodule.prog_symbol Why3.Wstdlib.Mstr.t;
    ns_xs : Why3.Ity.xsymbol Why3.Wstdlib.Mstr.t;
    ns_ns : Pmodule.namespace Why3.Wstdlib.Mstr.t;
  }
  val empty_ns : Pmodule.namespace
  val ns_find_prog_symbol :
    Pmodule.namespace -> string list -> Pmodule.prog_symbol
  val ns_find_its : Pmodule.namespace -> string list -> Why3.Ity.itysymbol
  val ns_find_pv : Pmodule.namespace -> string list -> Why3.Ity.pvsymbol
  val ns_find_xs : Pmodule.namespace -> string list -> Why3.Ity.xsymbol
  val ns_find_ns : Pmodule.namespace -> string list -> Pmodule.namespace
  val ns_find_rs : Pmodule.namespace -> string list -> Why3.Expr.rsymbol
  type overload = FixedRes of Why3.Ity.ity | SameType | NoOver
  val overload_of_rs : Why3.Expr.rsymbol -> Pmodule.overload
  val overload_of_oo : Why3.Expr.Srs.t -> Pmodule.overload
  val ref_attr : Why3.Ident.attribute
  exception IncompatibleNotation of string
  type pmodule0 = private {
    mod_theory : Why3.Theory.theory;
    mod_units : Pmodule.mod_unit list;
    mod_export : Pmodule.namespace;
    mod_known : Why3.Pdecl.known_map;
    mod_local : Why3.Ident.Sid.t;
    mod_used : Why3.Ident.Sid.t;
  }
  and mod_unit =
      Udecl of Why3.Pdecl.pdecl
    | Uuse of Pmodule.pmodule0
    | Uclone of Pmodule.mod_inst
    | Umeta of Why3.Theory.meta * Why3.Theory.meta_arg list
    | Uscope of string * Pmodule.mod_unit list
  and mod_inst = {
    mi_mod : Pmodule.pmodule0;
    mi_ty : Why3.Ity.ity Why3.Ty.Mts.t;
    mi_ts : Why3.Ity.itysymbol Why3.Ty.Mts.t;
    mi_ls : Why3.Term.lsymbol Why3.Term.Mls.t;
    mi_pr : Why3.Decl.prsymbol Why3.Decl.Mpr.t;
    mi_pk : Why3.Decl.prop_kind Why3.Decl.Mpr.t;
    mi_pv : Why3.Ity.pvsymbol Why3.Term.Mvs.t;
    mi_rs : Why3.Expr.rsymbol Why3.Expr.Mrs.t;
    mi_xs : Why3.Ity.xsymbol Why3.Ity.Mxs.t;
    mi_df : Why3.Decl.prop_kind;
  }
  type pmodule = private {
    mod_inst : Pmodule.mod_inst;
    mod_intf : Pmodule.pmodule0;
    mod_impl : Pmodule.pmodule0;
  }
  val mod_name : Pmodule.pmodule -> Why3.Ident.ident
  val mod_theory : Pmodule.pmodule -> Why3.Theory.theory
  val mod_export_intf : Pmodule.pmodule -> Pmodule.namespace
  val mod_export_impl : Pmodule.pmodule -> Pmodule.namespace
  val mod_known_intf : Pmodule.pmodule -> Why3.Pdecl.known_map
  val mod_known_impl : Pmodule.pmodule -> Why3.Pdecl.known_map
  val empty_mod_inst : Pmodule.pmodule -> Pmodule.mod_inst
  type pmodule_uc0 = private {
    muc_theory : Why3.Theory.theory_uc;
    muc_units : Pmodule.mod_unit list;
    muc_import : Pmodule.namespace list;
    muc_export : Pmodule.namespace list;
    muc_known : Why3.Pdecl.known_map;
    muc_local : Why3.Ident.Sid.t;
    muc_used : Why3.Ident.Sid.t;
    muc_env : Why3.Env.env;
  }
  type pmodule_uc = private {
    muc_intf : Pmodule.pmodule_uc0;
    muc_impl : Pmodule.pmodule_uc0;
  }
  val create_module :
    Why3.Env.env ->
    ?path:string list -> Why3.Ident.preid -> Pmodule.pmodule_uc
  val close_module : Pmodule.pmodule_uc -> Pmodule.pmodule
  val open_scope : Pmodule.pmodule_uc -> string -> Pmodule.pmodule_uc
  val close_scope : Pmodule.pmodule_uc -> import:bool -> Pmodule.pmodule_uc
  val import_scope : Pmodule.pmodule_uc -> string list -> Pmodule.pmodule_uc
  val restore_path : Why3.Ident.ident -> string list * string * string list
  val restore_module_id : Why3.Ident.ident -> Pmodule.pmodule
  val restore_module : Why3.Theory.theory -> Pmodule.pmodule
  val use_export :
    Pmodule.pmodule_uc -> Pmodule.pmodule -> Pmodule.pmodule_uc
  val clone_export :
    ?loc:Why3.Loc.position ->
    Pmodule.pmodule_uc ->
    Pmodule.pmodule -> Pmodule.mod_inst -> Pmodule.pmodule_uc
  val add_meta :
    Pmodule.pmodule_uc ->
    Why3.Theory.meta -> Why3.Theory.meta_arg list -> Pmodule.pmodule_uc
  val add_pdecl :
    ?warn:bool ->
    vc:bool -> Pmodule.pmodule_uc -> Why3.Pdecl.pdecl -> Pmodule.pmodule_uc
  val close_module_with_intf :
    Pmodule.pmodule_uc ->
    Pmodule.pmodule -> Pmodule.pmodule * Pmodule.pmodule
  val builtin_module : Pmodule.pmodule
  val bool_module : Pmodule.pmodule
  val unit_module : Pmodule.pmodule
  val highord_module : Pmodule.pmodule
  val tuple_module : int -> Pmodule.pmodule
  val ref_module : Pmodule.pmodule
  val its_ref : Why3.Ity.itysymbol
  val ts_ref : Why3.Ty.tysymbol
  val rs_ref : Why3.Expr.rsymbol
  val rs_ref_cons : Why3.Expr.rsymbol
  val rs_ref_proj : Why3.Expr.rsymbol
  val ls_ref_cons : Why3.Term.lsymbol
  val ls_ref_proj : Why3.Term.lsymbol
  type mlw_file = Pmodule.pmodule Why3.Wstdlib.Mstr.t
  val mlw_language : Pmodule.mlw_file Why3.Env.language
  val mlw_language_builtin : Why3.Env.pathname -> Pmodule.mlw_file
  exception ModuleNotFound of Why3.Env.pathname * string
  val read_module :
    Why3.Env.env -> Why3.Env.pathname -> string -> Pmodule.pmodule
  val print_unit : Stdlib.Format.formatter -> Pmodule.mod_unit -> unit
  val print_module : Stdlib.Format.formatter -> Pmodule.pmodule -> unit
end