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