Commit 23cfc266 authored by Sylvain Dailler's avatar Sylvain Dailler

Fixed replay.

parent 28cd7354
......@@ -839,7 +839,8 @@ let replay ~remove_obsolete ~use_steps c ~callback =
(fun _ _ -> count := !count + 1) session;
(* Replaying function *)
let replay_pa id pa =
let replay_pa pa =
let id = pa.parent in
let pr = pa.prover in
(* If use_steps, we give only steps as a limit *)
let limit =
......@@ -858,6 +859,6 @@ let replay ~remove_obsolete ~use_steps c ~callback =
(* Calling replay on all the proof_attempts of the session *)
Session_itp.session_iter_proof_attempt
(fun id pa -> replay_pa id pa) session
(fun _ pa -> replay_pa pa) session
end
......@@ -1047,7 +1047,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
| Save_file_req (name, text) ->
save_file name text;
| Get_task nid -> send_task nid
| Replay_req -> replay_session (); resend_the_tree ()
| Replay_req -> replay_session (); reload_session ()
| Interrupt_req -> C.interrupt ()
| Command_req (nid, cmd) ->
begin
......
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