* fold_tac has now a new parameter, which is the reduction to ``undo''

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 173c1c59d3195f374fe087513c8d188d411d9855..14a0dc8543a6a511c33ab5bee6428bcc417ab041 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -199,8 +199,14 @@ let simpl term =
  apply_tactic
   (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some term))
 
-let fold term =
- apply_tactic (ReductionTactics.fold_tac ~also_in_hypotheses:true ~term)
+let fold_whd term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+    ~also_in_hypotheses:true ~term)
+let fold_reduce term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce
+    ~also_in_hypotheses:true ~term)
 
   (* other tactics *)