Module Session_tools

module Session_tools: sig .. end

Generic tools that can be applied on sessions

val unknown_to_known_provers : Whyconf.config_prover Whyconf.Mprover.t ->
Whyconf.prover ->
Whyconf.Mprover.key list * Whyconf.Mprover.key list *
Whyconf.Mprover.key list

return others, same name, same version

val convert_unknown_prover : keygen:'a Session.keygen -> 'a Session.env_session -> unit

try to add new proof_attempt with known provers for all proof attempt with unknown provers

val filter_proof_attempt : ?notify:'key Session.notify ->
('key Session.proof_attempt -> bool) -> 'key Session.session -> unit

remove all the proof attempts that do not satisfy the given predicate

val transform_proof_attempt : ?notify:'key Session.notify ->
keygen:'key Session.keygen -> 'key Session.env_session -> string -> unit

replace all the proof attempts of the given session by the application of the given registered transformation followed by a proof_attempt with the same prover and time limit (but undone)