~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