Added buttons for new tactics Injection and Discriminate

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c1dc822b68761242022f9df50932748ebe0952ca..bdf78b28fa1c32a5b88b0cf246b0a07a084cfedd 100644 (file)
--- 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) ;