elim tactic: it needs two arguments, a term as well as a pattern

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

diff --git a/components/tactics/reductionTactics.ml b/components/tactics/reductionTactics.ml
index 754b2c0c5b49cca403f94a8e3bde1ee86f2c9798..5afc672695733cada18b7335705e1d360bec515b 100644 (file)
--- a/components/tactics/reductionTactics.ml
+++ b/components/tactics/reductionTactics.ml
@@ -118,6 +118,17 @@ let normalize_tac ~pattern =
  mk_tactic (reduction_tac
   ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
 
+let head_beta_reduce_tac ?delta ?upto ~pattern =
+ begin match upto with
+    | Some upto -> 
+         HLog.warn (Printf.sprintf "inside head_beta_reduce_tac %i" upto)
+    | None -> HLog.warn (Printf.sprintf "inside head_beta_reduce_tac none")
+ end;
+ 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