(*~comments:"comments"*)
~copyright:"Copyright (C) 2005, the HELM team"
~license:(String.concat "\n" (parse_txt_file "LICENSE"))
(*~comments:"comments"*)
~copyright:"Copyright (C) 2005, the HELM team"
~license:(String.concat "\n" (parse_txt_file "LICENSE"))
let get_devel_selected () =
match model#easy_mselection () with
| [[name;_]] -> MatitamakeLib.development_for_name name
let get_devel_selected () =
match model#easy_mselection () with
| [[name;_]] -> MatitamakeLib.development_for_name name
(tac_w_term (A.Transitivity (loc, hole)));
connect_button tbar#assumptionButton (tac (A.Assumption loc));
connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
(tac_w_term (A.Transitivity (loc, hole)));
connect_button tbar#assumptionButton (tac (A.Assumption loc));
connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
MatitaGtkMisc.toggle_widget_visibility
~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
~check:main#tacticsBarMenuItem;
MatitaGtkMisc.toggle_widget_visibility
~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
~check:main#tacticsBarMenuItem;
let selection = dialog#interpChoiceTreeView#selection in
ignore (selection#connect#changed (fun _ ->
match selection#get_selected_rows with
let selection = dialog#interpChoiceTreeView#selection in
ignore (selection#connect#changed (fun _ ->
match selection#get_selected_rows with