Commit 4dcb5f63 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Added get_prover_config in Whyconf.

This is more convenient when using only the Why3 API from SPARK for
parent 6cf8e120
......@@ -750,6 +750,8 @@ let save_config config =
let get_main config = config.main
let get_provers config = config.provers
let get_prover_config config prover =
Mprover.find prover (get_provers config)
let get_prover_shortcuts config = config.prover_shortcuts
let get_policies config = config.provers_upgrade_policy
let get_prover_upgrade_policy config p =
......@@ -127,6 +127,10 @@ val get_provers : config -> config_prover Mprover.t
(** [get_provers config] get the prover family stored in the Rc file. The
keys are the unique ids of the prover (argument of the family) *)
val get_prover_config: config -> prover -> config_prover
(** [get_prover_config config prover] get the prover config as stored in
the config. Raise Not_found if the prover does not exists in the config. *)
val set_provers : config ->
?shortcuts:prover Mstr.t -> config_prover Mprover.t -> config
(** [set_provers config provers] replace all the family prover by the
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment