diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml index 662b145ba0b734d61780820c951675c7db590c91..3732555a5f7497e62e251ab8467721a816ee256f 100644 --- a/src/plugins/wp/Stats.ml +++ b/src/plugins/wp/Stats.ml @@ -187,6 +187,7 @@ let pretty fmt s = let to_json_p (p,r) : Json.t = `Assoc [ "prover", `String (VCS.name_of_prover p) ; + "hprover", `String (VCS.title_of_prover p) ; "time", `Float r.time ; "htime", `String (Pretty_utils.to_string Rformat.pp_time r.time) ; "success", `Int r.success ; diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml index 07645004d587aa7a93c6f4fa1f722b17d2029043..167dc3e1370b6261b1861de7846aaf73e0402c48 100644 --- a/src/plugins/wp/Why3Provers.ml +++ b/src/plugins/wp/Why3Provers.ml @@ -93,7 +93,7 @@ let print_wp s = let prv = String.split_on_char ',' name in String.concat ":" prv -let title p = Format.asprintf "%a" Why3.Whyconf.print_prover p +let title p = Pretty_utils.to_string Why3.Whyconf.print_prover p let name p = p.Why3.Whyconf.prover_name let compare = Why3.Whyconf.Prover.compare let is_mainstream p = p.Why3.Whyconf.prover_altern = ""