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