X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FreductionTactics.ml;h=685baff9be8ecea7dfb4885ad9965bd8b7aa8199;hb=12fe61bed1275c4c596501fb951a9197f50c93e8;hp=754b2c0c5b49cca403f94a8e3bde1ee86f2c9798;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 754b2c0c5..685baff9b 100644
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -118,6 +118,12 @@ let normalize_tac ~pattern =
  mk_tactic (reduction_tac
   ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
 
+let head_beta_reduce_tac ?delta ?upto ~pattern =
+ mk_tactic (reduction_tac
+  ~reduction:
+    (const_lazy_reduction
+      (fun _context -> CicReduction.head_beta_reduce ?delta ?upto)) ~pattern)
+
 exception NotConvertible
 
 (* Note: this code is almost identical to reduction_tac and