X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FproofEngine.ml;h=73e2aa177dfa76a0d8280b8f0813bf4f52e3d602;hb=a772e377c1ca7c43c3e1e25eb47479fc3c5ceb9e;hp=14a0dc8543a6a511c33ab5bee6428bcc417ab041;hpb=ba712be83ed64a934037e2310aa5bdef25e9d3b9;p=helm.git

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