New tactic fold_simpl.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 4878088b709748ef9bc5d0168965420ebe5985a9..afbbc143919ccf8fd96bd68974779eae76a3802b 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2272,6 +2272,7 @@ let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
+let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
 let cut = call_tactic_with_input ProofEngine.cut;;
 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
 let letin = call_tactic_with_input ProofEngine.letin;;
@@ -2710,14 +2711,17 @@ object(self)
    let simplb =
     GButton.button ~label:"Simpl"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let hbox4 =
-    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let foldwhdb =
     GButton.button ~label:"Fold_whd"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox4 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let foldreduceb =
     GButton.button ~label:"Fold_reduce"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   let foldsimplb =
+    GButton.button ~label:"Fold_simpl"
+     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
    let cutb =
     GButton.button ~label:"Cut"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2792,6 +2796,7 @@ object(self)
    ignore(simplb#connect#clicked simpl) ;
    ignore(foldwhdb#connect#clicked fold_whd) ;
    ignore(foldreduceb#connect#clicked fold_reduce) ;
+   ignore(foldsimplb#connect#clicked fold_simpl) ;
    ignore(cutb#connect#clicked cut) ;
    ignore(changeb#connect#clicked change) ;
    ignore(letinb#connect#clicked letin) ;