Module Why3_session

module Why3_session: sig .. end
From the original file we kept only the reading of a session. We also discard all the information about how that have been proved (metas, transformation, proof_attempts) or the order of the goals

Not mutated after the creation



Proof attempts


type goal = private {
   goal_name : string;
   goal_parent : theory;
   mutable goal_verified : bool;
}
type theory = private {
   theory_name : string;
   theory_parent : file;
   theory_goals : goal Datatype.String.Hashtbl.t;
   mutable theory_verified : bool;
}
type file = private {
   file_name : string;
   file_format : string option;
   file_parent : session;
   file_theories : theory Datatype.String.Hashtbl.t; (*
Not mutated after the creation

Not mutated after the creation

*)
   mutable file_verified : bool;
}
type session = private {
   session_files : file Datatype.String.Hashtbl.t;
   session_dir : string;
}
exception LoadError

Read/Write


val read_session : string -> session
Read a session stored on the disk. It returns a session without any task attached to goals