sig
  type goal = private {
    goal_name : string;
    goal_parent : Why3_session.theory;
    mutable goal_verified : bool;
  }
  and theory = private {
    theory_name : string;
    theory_parent : Why3_session.file;
    theory_goals : Why3_session.goal Datatype.String.Hashtbl.t;
    mutable theory_verified : bool;
  }
  and file = private {
    file_name : string;
    file_format : string option;
    file_parent : Why3_session.session;
    file_theories : Why3_session.theory Datatype.String.Hashtbl.t;
    mutable file_verified : bool;
  }
  and session = private {
    session_files : Why3_session.file Datatype.String.Hashtbl.t;
    session_dir : string;
  }
  exception LoadError
  val read_session : string -> Why3_session.session
end