Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 761eaec6 authored by MARCHE Claude's avatar MARCHE Claude

itp: micro detail

parent b0c1616a
......@@ -852,19 +852,6 @@ let replay ~remove_obsolete ~use_steps c ~callback ~notification ~final_callback
| Uninstalled _ -> r := (id, pr, limits, Prover_not_installed) :: !r;
in
(*
let update_node pa s callback =
match s with
| Done new_r ->
(pa.Session_itp.proof_state <- Some new_r;
pa.proof_obsolete <- false)
| InternalFailure _ ->
pa.proof_obsolete <- true
| Uninstalled _ ->
pa.proof_obsolete <- true
| _ -> assert false in
*)
let update_uninstalled c remove_obsolete id s pr =
match s with
| Uninstalled _ ->
......@@ -899,9 +886,6 @@ let replay ~remove_obsolete ~use_steps c ~callback ~notification ~final_callback
~callback:(fun id s ->
counting s count;
craft_report s report parid pr limit pa;
(*
update_node pa s ~callback ~notification;
*)
update_uninstalled c remove_obsolete parid s pr;
callback id s;
if !count = 0 then final_callback !report)
......
......@@ -249,7 +249,6 @@ val replay_print:
(proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list ->
unit
(* TODO replay for manual proofs ? *)
val replay:
remove_obsolete:bool ->
(** If true, removes obsolete attempt in all cases. Otherwise keep it in
......
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