X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=f5c82a9fe7da0be3f2702d90c5733a99cc3c6f4d;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=1885e956cf36191dd74bf18d08264915bd41aacb;hpb=bf40c378bd2c624405be2118a478a0734eb8d3aa;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 1885e956c..f5c82a9fe 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -73,16 +73,20 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
   (curi,metasenv',pbo,pty), [metano]
 ;;
 
-let simpl_tac ~pattern = 
+let simpl_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
 
-let reduce_tac ~pattern = 
+let reduce_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
+
+let unfold_tac what ~pattern =
+ mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
+  ~pattern);;
   
-let whd_tac ~pattern = 
+let whd_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
 
-let normalize_tac ~pattern = 
+let normalize_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
 
 exception NotConvertible