Commit 7fe487b6 authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] fix prover title

parent b80a7162
......@@ -207,7 +207,8 @@ let pp_stats fmt s =
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
Format.fprintf fmt " (%a" VCS.pp_prover p ;
let title = VCS.title_of_prover ~version:false p in
Format.fprintf fmt " (%s" title ;
if success > 0 && np > 1 then
Format.fprintf fmt " %d/%d" success np ;
if not shell && pr.time > Rformat.epsilon then
......
......@@ -79,9 +79,12 @@ let name_of_prover = function
| Qed -> "qed"
| Tactical -> "script"
let title_of_prover = function
let title_of_prover ?version = function
| Why3 s ->
if Wp_parameters.has_dkey dkey_shell
let v = match version with Some v -> v | None ->
Wp_parameters.has_dkey dkey_shell
in
if v
then Why3Provers.name s
else Why3Provers.title s
| Qed -> "Qed"
......
......@@ -42,7 +42,7 @@ module Pset : Set.S with type elt = prover
module Pmap : Map.S with type key = prover
val name_of_prover : prover -> string
val title_of_prover : prover -> string
val title_of_prover : ?version:bool -> prover -> string
val filename_for_prover : prover -> string
val title_of_mode : mode -> string
......
Supports Markdown
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