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)