*)
type direction = [ `Left | `Right ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd ]
+type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
(* type 'term pattern = Pattern of 'term *)
(* everywhere includes goal and hypotheses *)
| LetIn of loc * 'term * 'ident
(* | Named_intros of loc * 'ident list (* joined with Intros above *) *)
(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
+ | ReduceAt of loc * reduction_kind * 'ident * 'term
| Reduce of loc * reduction_kind * ('term list * 'term pattern) option
(* kind, (what, where)
* if second argument is None, reduction is applied to the current goal,