let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
let cut = call_tactic_with_input ProofEngine.cut;;
let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
let letin = call_tactic_with_input ProofEngine.letin;;
let cut = call_tactic_with_input ProofEngine.cut;;
let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
let letin = call_tactic_with_input ProofEngine.letin;;
ignore(simplb#connect#clicked simpl) ;
ignore(foldwhdb#connect#clicked fold_whd) ;
ignore(foldreduceb#connect#clicked fold_reduce) ;
ignore(simplb#connect#clicked simpl) ;
ignore(foldwhdb#connect#clicked fold_whd) ;
ignore(foldreduceb#connect#clicked fold_reduce) ;
ignore(cutb#connect#clicked cut) ;
ignore(changeb#connect#clicked change) ;
ignore(letinb#connect#clicked letin) ;
ignore(cutb#connect#clicked cut) ;
ignore(changeb#connect#clicked change) ;
ignore(letinb#connect#clicked letin) ;