*)
type direction = [ `LeftToRight | `RightToLeft ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
+type 'term reduction_kind =
+ [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
type loc = CicNotationPt.location
| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
+ | Fold of loc * 'term reduction_kind * 'term * ('term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * string * 'ident list
| Generalize of loc * ('term, 'ident) pattern * 'ident option
| LApply of loc * int option * 'term list * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
- | Reduce of loc * reduction_kind * ('term, 'ident) pattern
+ | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern
| Reflexivity of loc
| Replace of loc * ('term, 'ident) pattern * 'term
| Rewrite of loc * direction * 'term * ('term, 'ident) pattern