*)
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,
| WLocate of loc * string
| WElim of loc * 'term
(* real macros *)
- | Abort of loc
+(* | Abort of loc *)
| Print of loc * string
| Check of loc * 'term
| Hint of loc
| Quit of loc
- | Redo of loc * int option
- | Undo of loc * int option
+(* | Redo of loc * int option
+ | Undo of loc * int option *)
(* | Print of loc * print_kind *)
| Search_pat of loc * search_kind * string (* searches with string pattern *)
| Search_term of loc * search_kind * 'term (* searches with term pattern *)