X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=746ef8ffa67c74c7bdc455ca7e23d25e0d976d4e;hb=e362056c17a503d3ac47600db90de1c534fb1fbb;hp=1d636ef8b88e7e63865f9b7cb45d59a7b5273cd7;hpb=5b72c06c73ae9493ef7df7f8ca10fd95d02983e1;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 1d636ef8b..746ef8ffa 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -268,9 +268,13 @@ object (self)
       GMenu.image_menu_item ?stock ?label ~packing:menu#append () in
     let check = add_menu_item ~label:"Check" () in
     let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in
+    let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in
     menu#append reductions_menu_item;
+    menu#append tactics_menu_item;
     let reductions = GMenu.menu () in
+    let tactics = GMenu.menu () in
     reductions_menu_item#set_submenu reductions;
+    tactics_menu_item#set_submenu tactics;
     let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
     let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in
     let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in