sig   type prover = Why3 of string | Why3ide | AltErgo | Coq | Qed   type mode = BatchMode | EditMode | FixMode   type language = L_why3 | L_coq | L_altergo   module Pmap :     sig       type key = prover       type +'a t       val empty : 'a t       val is_empty : 'a t -> bool       val mem : key -> 'a t -> bool       val add : key -> '-> 'a t -> 'a t       val singleton : key -> '-> 'a t       val remove : key -> 'a t -> 'a t       val merge :         (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t       val union : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t       val compare : ('-> '-> int) -> 'a t -> 'a t -> int       val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool       val iter : (key -> '-> unit) -> 'a t -> unit       val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b       val for_all : (key -> '-> bool) -> 'a t -> bool       val exists : (key -> '-> bool) -> 'a t -> bool       val filter : (key -> '-> bool) -> 'a t -> 'a t       val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t       val cardinal : 'a t -> int       val bindings : 'a t -> (key * 'a) list       val min_binding : 'a t -> key * 'a       val max_binding : 'a t -> key * 'a       val choose : 'a t -> key * 'a       val split : key -> 'a t -> 'a t * 'a option * 'a t       val find : key -> 'a t -> 'a       val map : ('-> 'b) -> 'a t -> 'b t       val mapi : (key -> '-> 'b) -> 'a t -> 'b t     end   val language_of_prover : Wp.VCS.prover -> Wp.VCS.language   val language_of_name : string -> Wp.VCS.language option   val name_of_prover : Wp.VCS.prover -> string   val filename_for_prover : Wp.VCS.prover -> string   val prover_of_name : string -> Wp.VCS.prover option   val language_of_prover_name : string -> Wp.VCS.language option   val mode_of_prover_name : string -> Wp.VCS.mode   val name_of_mode : Wp.VCS.mode -> string   val pp_prover : Format.formatter -> Wp.VCS.prover -> unit   val pp_language : Format.formatter -> Wp.VCS.language -> unit   val pp_mode : Format.formatter -> Wp.VCS.mode -> unit   val cmp_prover : Wp.VCS.prover -> Wp.VCS.prover -> int   type verdict =       NoResult     | Invalid     | Unknown     | Timeout     | Stepout     | Computing of (unit -> unit)     | Checked     | Valid     | Failed   type result = {     verdict : Wp.VCS.verdict;     solver_time : float;     prover_time : float;     prover_steps : int;     prover_errpos : Lexing.position option;     prover_errmsg : string;   }   val no_result : Wp.VCS.result   val valid : Wp.VCS.result   val checked : Wp.VCS.result   val invalid : Wp.VCS.result   val unknown : Wp.VCS.result   val stepout : Wp.VCS.result   val timeout : int -> Wp.VCS.result   val computing : (unit -> unit) -> Wp.VCS.result   val failed : ?pos:Lexing.position -> string -> Wp.VCS.result   val kfailed :     ?pos:Lexing.position ->     ('a, Format.formatter, unit, Wp.VCS.result) Pervasives.format4 -> 'a   val result :     ?solver:float ->     ?time:float -> ?steps:int -> Wp.VCS.verdict -> Wp.VCS.result   val is_verdict : Wp.VCS.result -> bool   val pp_result : Format.formatter -> Wp.VCS.result -> unit   val compare : Wp.VCS.result -> Wp.VCS.result -> int end