]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/proofEngine.ml
*** empty log message ***
[helm.git] / helm / gTopLevel / proofEngine.ml
index 173c1c59d3195f374fe087513c8d188d411d9855..73e2aa177dfa76a0d8280b8f0813bf4f52e3d602 100644 (file)
@@ -199,8 +199,18 @@ 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)
+let fold_simpl term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl
+    ~also_in_hypotheses:true ~term)
 
   (* other tactics *)