X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2FreductionTactics.ml;h=685baff9be8ecea7dfb4885ad9965bd8b7aa8199;hb=e05e28d01c55699ce539699ac745341bfa4c1c0f;hp=754b2c0c5b49cca403f94a8e3bde1ee86f2c9798;hpb=e00d05ab58597620345c2fd49b84a23efa8db34c;p=helm.git

diff --git a/components/tactics/reductionTactics.ml b/components/tactics/reductionTactics.ml
index 754b2c0c5..685baff9b 100644
--- a/components/tactics/reductionTactics.ml
+++ b/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