Commit 95ba51b7 authored by MARCHE Claude's avatar MARCHE Claude

fix obsolete status and proved status during replay

parent b7dbd0e5
......@@ -563,7 +563,7 @@ let schedule_proof_attempt_r c id pr ~counterexmp ~limit ~callback =
let schedule_proof_attempt c id pr ~counterexmp ~limit ~callback ~notification =
let callback panid s = callback panid s;
(match s with
| Scheduled | Done _ -> update_goal_node notification c id
| Scheduled | Running | Done _ -> update_goal_node notification c id
| _ -> ())
in
schedule_proof_attempt_r c id pr ~counterexmp ~limit ~callback
......
......@@ -534,7 +534,7 @@ let graft_proof_attempt (s : session) (id : proofNodeID) (pr : Whyconf.prover)
try
let id = Hprover.find pn.proofn_attempts pr in
let pa = Hint.find s.proofAttempt_table id in
let pa = { pa with limit = limit; proof_obsolete = true } in
let pa = { pa with limit = limit; proof_state = None; proof_obsolete = false } in
Hint.replace s.proofAttempt_table id pa;
id
with Not_found ->
......@@ -672,9 +672,10 @@ let update_proof_attempt s id pr st =
let n = get_proofNode s id in
let pa = Hprover.find n.proofn_attempts pr in
let pa = get_proof_attempt_node s pa in
pa.proof_state <- Some st
pa.proof_state <- Some st;
pa.proof_obsolete <- false
with
| BadID when not (Debug.test_flag debug_stack_trace) -> ()
| BadID when not (Debug.test_flag debug_stack_trace) -> assert false
(****************************)
(* session opening *)
......
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