subst tactic put in a file on its own

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

diff --git a/components/tactics/reductionTactics.ml b/components/tactics/reductionTactics.ml
index 754b2c0c5b49cca403f94a8e3bde1ee86f2c9798..685baff9be8ecea7dfb4885ad9965bd8b7aa8199 100644 (file)
--- 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