paths trough terms implemented with a nice hack :)

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

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index d356499a1d50fccad761e5c7ed7d3adb8d2ae6f6..d3d36ca6e9cf630cfd64e93ea07e732a8df3973f 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -103,6 +103,10 @@ let whd_tac ~also_in_hypotheses ~terms =
  mk_tactic ( reduction_tac ~reduction:CicReduction.whd 
   ~also_in_hypotheses ~terms);;
 
+let normalize_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:CicReduction.normalize 
+  ~also_in_hypotheses ~terms);;
+
 let fold_tac ~reduction ~also_in_hypotheses ~term =
  let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
   let curi,metasenv,pbo,pty = proof in