X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=d3d36ca6e9cf630cfd64e93ea07e732a8df3973f;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=d356499a1d50fccad761e5c7ed7d3adb8d2ae6f6;hpb=d9bd1adaa8588112818d3b6977a5c42a03755a21;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index d356499a1..d3d36ca6e 100644
--- 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