- ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ())));
- ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply));
- ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact));
- ignore (tbar#elimButton#connect#clicked (tac_w_term "elim"
- Tactics.elim_intros_simpl));
- ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type"
- Tactics.elim_type));
- ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split));
- ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left));
- ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right));
- ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists));
- ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity"
- Tactics.reflexivity));
- ignore (tbar#symmetryButton#connect#clicked (tac "symmetry"
- Tactics.symmetry));
- ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity"
- Tactics.transitivity));
- ignore (tbar#assumptionButton#connect#clicked (tac "assumption"
- Tactics.assumption));
- ignore (tbar#cutButton#connect#clicked (tac_w_term "cut"
- (Tactics.cut ?mk_fresh_name_callback:None)));
- ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd)))
+ 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#simplifyButton FINQUI; *)
+
+ connect_button tbar#assumptionButton (tac A.Assumption);
+ connect_button tbar#cutButton (tac_w_term (A.Cut hole));
+ connect_button tbar#autoButton (tac A.Auto)