| Fold of loc * reduction_kind * 'term
| Fourier of loc
| FwdSimpl of loc * 'term
- | Generalize of loc * 'term * ('term, 'ident) pattern
+ | Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
| Injection of loc * 'term
| Intros of loc * int option * 'ident list