From: Claudio Sacerdoti Coen 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