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 : VCS.prover -> VCS.language   val language_of_name : string -> VCS.language option   val name_of_prover : VCS.prover -> string   val filename_for_prover : VCS.prover -> string   val prover_of_name : string -> VCS.prover option   val language_of_prover_name : string -> VCS.language option   val mode_of_prover_name : string -> VCS.mode   val name_of_mode : VCS.mode -> string   val pp_prover : Format.formatter -> VCS.prover -> unit   val pp_language : Format.formatter -> VCS.language -> unit   val pp_mode : Format.formatter -> VCS.mode -> unit   val cmp_prover : VCS.prover -> VCS.prover -> int   type verdict =       NoResult     | Invalid     | Unknown     | Timeout     | Stepout     | Computing of (unit -> unit)     | Checked     | Valid     | Failed   type result = {     verdict : VCS.verdict;     solver_time : float;     prover_time : float;     prover_steps : int;     prover_errpos : Lexing.position option;     prover_errmsg : string;   }   val no_result : VCS.result   val valid : VCS.result   val checked : VCS.result   val invalid : VCS.result   val unknown : VCS.result   val stepout : VCS.result   val timeout : int -> VCS.result   val computing : (unit -> unit) -> VCS.result   val failed : ?pos:Lexing.position -> string -> VCS.result   val kfailed :     ?pos:Lexing.position ->     ('a, Format.formatter, unit, VCS.result) Pervasives.format4 -> 'a   val result :     ?solver:float -> ?time:float -> ?steps:int -> VCS.verdict -> VCS.result   val is_verdict : VCS.result -> bool   val pp_result : Format.formatter -> VCS.result -> unit   val compare : VCS.result -> VCS.result -> int end