New tactic fold_simpl.

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) ;

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 14a0dc8543a6a511c33ab5bee6428bcc417ab041..73e2aa177dfa76a0d8280b8f0813bf4f52e3d602 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -207,6 +207,10 @@ let fold_reduce term =
  apply_tactic
   (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce
     ~also_in_hypotheses:true ~term)
+let fold_simpl term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl
+    ~also_in_hypotheses:true ~term)
 
   (* other tactics *)
 

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 710f8efacfad39a52c031fad2959f8d5730cd7b6..73dcb4d75c6c6b5a6b4777d4266faaff70813396 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -36,6 +36,7 @@ val reduce : Cic.term -> unit
 val simpl : Cic.term -> unit
 val fold_whd : Cic.term -> unit
 val fold_reduce : Cic.term -> unit
+val fold_simpl : Cic.term -> unit
 
   (* scratch area reduction tactics *)
 val whd_in_scratch : Cic.term -> Cic.term -> Cic.term