X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=bdf78b28fa1c32a5b88b0cf246b0a07a084cfedd;hb=e974eb6799c994efdee15aa47a34909360dc0aec;hp=c1dc822b68761242022f9df50932748ebe0952ca;hpb=7bf5d654c18fee290e7e402800543fe40223c04b;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c1dc822b6..bdf78b28f 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2538,6 +2538,12 @@ object(self)
    let replaceb =
     GButton.button ~label:"Replace"
      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let injectionb =
+    GButton.button ~label:"Injection"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let discriminateb =
+    GButton.button ~label:"Discriminate"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
 (* Zack: spostare in una toolbar
    let generalizeb =
     GButton.button ~label:"Generalize"
@@ -2587,6 +2593,8 @@ object(self)
    ignore(introsb#connect#clicked InvokeTactics'.intros) ;
    ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
+   ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
+   ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
 (* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;