Commit 5b50a150 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Changed th_proved to be able to see theories with no goals as proved.

parent c80328b7
......@@ -72,7 +72,11 @@ let create_controller env s = {
let tn_proved c tid = Htn.find_def c.proof_state.tn_state false tid
let pn_proved c pid = Hpn.find_def c.proof_state.pn_state false pid
let th_proved c th = Hid.find_def c.proof_state.th_state false th
let th_proved c th =
if (theory_goals th = []) then
Hid.find_def c.proof_state.th_state true (theory_name th)
else
Hid.find_def c.proof_state.th_state false (theory_name th)
(* Update the result of the theory according to its children *)
let update_theory th ps =
......@@ -147,7 +151,7 @@ module PSession = struct
| Theory th ->
let id = theory_name th in
let name = id.Ident.id_string in
let name = if th_proved x.tcont id then name^"!" else name^"?" in
let name = if th_proved x.tcont th then name^"!" else name^"?" in
name,
List.fold_right (fun g -> n (Goal g)) (theory_goals th)
(List.fold_right (fun g -> n (Goal g)) (theory_detached_goals th) [])
......
......@@ -86,7 +86,7 @@ val update_trans_node: controller -> Session_itp.transID -> bool -> unit
(** Used to find if a proof/trans node or theory is proved or not *)
val tn_proved: controller -> Session_itp.transID -> bool
val pn_proved: controller -> Session_itp.proofNodeID -> bool
val th_proved: controller -> Ident.ident -> bool
val th_proved: controller -> Session_itp.theory -> bool
val print_session : Format.formatter -> controller -> unit
......
......@@ -425,7 +425,7 @@ and print_trans_node s fmt id =
(Pp.print_list Pp.semi (print_proof_node s)) ll
let print_theory s fmt th : unit =
if Controller_itp.th_proved cont (theory_name th) then
if Controller_itp.th_proved cont th then
fprintf fmt "P";
fprintf fmt "@[<hv 1> Theory %s;@ [%a];@ detached[%a]@]" (theory_name th).Ident.id_string
(Pp.print_list Pp.semi (print_proof_node s)) (theory_goals th)
......
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