* fold_tac has now a new parameter, which is the reduction to ``undo''

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index a6dfd3a7b74a2f6656f2505564e70f1a84919dff..4878088b709748ef9bc5d0168965420ebe5985a9 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2270,7 +2270,8 @@ let elimtype = call_tactic_with_input ProofEngine.elim_type;;
 let whd = call_tactic_with_goal_input ProofEngine.whd;;
 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
-let fold = call_tactic_with_input ProofEngine.fold;;
+let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
+let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
 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;;
@@ -2709,14 +2710,17 @@ object(self)
    let simplb =
     GButton.button ~label:"Simpl"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let foldb =
-    GButton.button ~label:"Fold"
-     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let cutb =
-    GButton.button ~label:"Cut"
-     ~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
+   let foldreduceb =
+    GButton.button ~label:"Fold_reduce"
+     ~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
    let changeb =
     GButton.button ~label:"Change"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2732,17 +2736,17 @@ object(self)
    let clearb =
     GButton.button ~label:"Clear"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox5 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let fourierb =
     GButton.button ~label:"Fourier"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let rewritesimplb =
     GButton.button ~label:"RewriteSimpl ->"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let reflexivityb =
     GButton.button ~label:"Reflexivity"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let hbox5 =
-    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let symmetryb =
     GButton.button ~label:"Symmetry"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2755,20 +2759,20 @@ object(self)
    let splitb =
     GButton.button ~label:"Split"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox6 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let leftb =
     GButton.button ~label:"Left"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let rightb =
     GButton.button ~label:"Right"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let assumptionb =
     GButton.button ~label:"Assumption"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let generalizeb =
     GButton.button ~label:"Generalize"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-   let hbox6 =
-    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let absurdb =
     GButton.button ~label:"Absurd"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2786,7 +2790,8 @@ object(self)
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
    ignore(simplb#connect#clicked simpl) ;
-   ignore(foldb#connect#clicked fold) ;
+   ignore(foldwhdb#connect#clicked fold_whd) ;
+   ignore(foldreduceb#connect#clicked fold_reduce) ;
    ignore(cutb#connect#clicked cut) ;
    ignore(changeb#connect#clicked change) ;
    ignore(letinb#connect#clicked letin) ;