+ f)));
+ ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
+ ignore (MatitaMathView.cicBrowser ())));
+ let module A = TacticAst in
+ let hole = CicAst.UserInput in
+ let tac ast _ =
+ let ast = A.Tactic ast in
+ ignore (script#advance (TacticAstPp.pp_tactical ast))
+ in
+ let tac_w_term ast _ =
+(* gui#console#clear (); *)
+ gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
+ gui#main#mainWin#present ()
+ in
+ let tbar = gui#toolbar in
+ connect_button tbar#introsButton (tac (A.Intros (None, [])));
+ connect_button tbar#applyButton (tac_w_term (A.Apply hole));
+ connect_button tbar#exactButton (tac_w_term (A.Exact hole));
+ connect_button tbar#elimButton (tac_w_term (A.Elim (hole, None)));
+ connect_button tbar#elimTypeButton (tac_w_term (A.ElimType hole));
+ connect_button tbar#splitButton (tac A.Split);
+ connect_button tbar#leftButton (tac A.Left);
+ connect_button tbar#rightButton (tac A.Right);
+ connect_button tbar#existsButton (tac A.Exists);
+ connect_button tbar#reflexivityButton (tac A.Reflexivity);
+ connect_button tbar#symmetryButton (tac A.Symmetry);
+ connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole));
+ connect_button tbar#assumptionButton (tac A.Assumption);
+ connect_button tbar#cutButton (tac_w_term (A.Cut hole));
+ connect_button tbar#autoButton (tac A.Auto)