Commit 92ba52cb authored by David Hauzar's avatar David Hauzar

Bugfix: mark edited proof as obsolete if the answer of prover is unknown.

If the answer of prover was unknown and reason of the answer was not None
and the proof was edited, it was not marked as obsolete. This commit
fixes this problem.

Contributed by Stefan Berghofer.
parent 01fab6cc
......@@ -862,7 +862,7 @@ let edit_proof ~cntexample eS sched ~default_editor a =
else
let callback a res =
match res with
| Done {Call_provers.pr_answer = Call_provers.Unknown ("", None)} ->
| Done {Call_provers.pr_answer = Call_provers.Unknown ("", _)} ->
set_proof_state ~notify ~obsolete:true ~archived:false
JustEdited a
| _ ->
......@@ -874,7 +874,7 @@ let edit_proof ~cntexample eS sched ~default_editor a =
let edit_proof_v3 ~cntexample eS sched ~default_editor ~callback a =
let callback a res =
match res with
| Done {Call_provers.pr_answer = Call_provers.Unknown ("", None)} ->
| Done {Call_provers.pr_answer = Call_provers.Unknown ("", _)} ->
callback a
| _ -> ()
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