Commit 60ae0d38 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'fix_correct_on_detached' into 'master'

itp_server: make attempt on detached goal appear detached

See merge request !251
parents e14007f7 9c446286
......@@ -721,13 +721,16 @@ end
| APa pa ->
let pa = get_proof_attempt_node s pa in
let obs = pa.proof_obsolete in
let detached = get_node_detached node in
let appear_obs = obs || detached in
let limit = pa.limit in
let res =
match pa.Session_itp.proof_state with
| Some pa -> Done pa
| _ -> Undone
in
P.notify (Node_change (new_id, Proof_status_change(res, obs, limit)))
P.notify (Node_change (new_id,
Proof_status_change(res, appear_obs, limit)))
(*
......
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