New tactic fold_simpl.

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

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