New tactic unfold.

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

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 1885e956cf36191dd74bf18d08264915bd41aacb..492b265cb5b3e97e0a26077b402104bb673430e5 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