From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Dec 2002 10:57:07 +0000 (+0000)
Subject: New tactic fold_simpl.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7d05aa09759ebf31f2df81b33051d6b3e463f52;p=helm.git

New tactic fold_simpl.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 4878088b7..afbbc1439 100644
--- 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 14a0dc854..73e2aa177 100644
--- 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 710f8efac..73dcb4d75 100644
--- 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