Commit 3141e44f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Just edited proofs can be played with 'replay' button

parent d861d947
This diff is collapsed.
......@@ -757,19 +757,11 @@ let edit_proof eS sched ~default_editor a =
O.init a.proof_key (Proof_attempt a);
a in
(** Now [a] is a proof_attempt of the lodable prover [nap] *)
let old_res = a.proof_state in
let callback res =
match res with
| Done _ ->
begin
match old_res with
| Undone Unedited ->
set_proof_state ~notify ~obsolete:true ~archived:false
(Undone JustEdited) a
| _ ->
set_proof_state ~notify ~obsolete:true ~archived:false
old_res a
end
set_proof_state ~notify ~obsolete:true ~archived:false
(Undone JustEdited) a
| _ ->
set_proof_state ~notify ~obsolete:false ~archived:false
res a
......
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