reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
menu#append (GMenu.separator_item ());
let copy = add_menu_item ~stock:`COPY () in
let gui = get_gui () in
List.iter (fun item -> item#misc#set_sensitive gui#canCopy)
let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
menu#append (GMenu.separator_item ());
let copy = add_menu_item ~stock:`COPY () in
let gui = get_gui () in
List.iter (fun item -> item#misc#set_sensitive gui#canCopy)
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
connect_menu_item simplify (reduction_action `Simpl);
connect_menu_item whd (reduction_action `Whd);
menu#popup ~button:right_button ~time
connect_menu_item simplify (reduction_action `Simpl);
connect_menu_item whd (reduction_action `Whd);
menu#popup ~button:right_button ~time