sig
  type fformat = string
  type filename = string
  type extension = string
  type pathname = string list
  type env
  val env_tag : Env.env -> Weakhtbl.tag
  module Wenv :
    sig
      type key = env
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> '-> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  val create_env : Env.filename list -> Env.env
  val get_loadpath : Env.env -> Env.filename list
  type 'a language
  val base_language : Theory.theory Wstdlib.Mstr.t Env.language
  val register_language : 'Env.language -> ('-> 'a) -> 'Env.language
  val add_builtin : 'Env.language -> (Env.pathname -> 'a) -> unit
  val base_language_builtin : Env.pathname -> Theory.theory Wstdlib.Mstr.t
  type 'a format_parser =
      Env.env -> Env.pathname -> Env.filename -> Stdlib.in_channel -> 'a
  exception KnownFormat of Env.fformat
  val register_format :
    desc:Pp.formatted ->
    'Env.language ->
    Env.fformat -> Env.extension list -> 'Env.format_parser -> unit
  val list_formats :
    'Env.language -> (Env.fformat * Env.extension list * Pp.formatted) list
  val get_format : ?format:Env.fformat -> string -> Env.fformat
  exception InvalidFormat of Env.fformat
  exception UnknownFormat of Env.fformat
  exception UnknownExtension of Env.extension
  exception UnspecifiedFormat
  val read_channel :
    ?format:Env.fformat ->
    'Env.language -> Env.env -> Env.filename -> Stdlib.in_channel -> 'a
  val read_file :
    ?format:Env.fformat ->
    'Env.language -> Env.env -> Env.filename -> 'a * Env.fformat
  exception LibraryNotFound of Env.pathname
  exception LibraryConflict of Env.pathname
  exception AmbiguousPath of Env.filename * Env.filename
  val read_library : 'Env.language -> Env.env -> Env.pathname -> 'a
  val locate_library : Env.env -> Env.pathname -> Env.filename
  exception TheoryNotFound of Env.pathname * string
  val read_theory : Env.env -> Env.pathname -> string -> Theory.theory
end