more work

[helm.git] / helm / software / matita / matitaMathView.ml

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index ff79f54ed05ee8d59a7bcfde9a1bff29538eef76..7f1917cfe1cf5ce6c3642966aaebd54ad1846546 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -288,14 +288,13 @@ object (self)
     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
     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)
-      [ copy; check; normalize; reduce; simplify; whd ];
+      [ copy; check; normalize; simplify; whd ];
     let reduction_action kind () =
       let pat = self#tactic_text_pattern_of_selection in
       let statement =
@@ -311,7 +310,6 @@ object (self)
       (MatitaScript.current ())#advance ~statement () in
     connect_menu_item copy gui#copy;
     connect_menu_item normalize (reduction_action `Normalize);
-    connect_menu_item reduce (reduction_action `Reduce);
     connect_menu_item simplify (reduction_action `Simpl);
     connect_menu_item whd (reduction_action `Whd);
     menu#popup ~button:right_button ~time