changed default parameter values...

[helm.git] / helm / ocaml / tactics / reductionTactics.ml

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 1885e956cf36191dd74bf18d08264915bd41aacb..f5c82a9fe7da0be3f2702d90c5733a99cc3c6f4d 100644 (file)
--- 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