| Apply of loc * 'term
| Auto of loc * int option
| Assumption of loc
- | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
+ | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *)
| Contradiction of loc
| Cut of loc * 'term
- | Decompose of loc * 'ident * 'ident list (* where, which principles *)
+ | Decompose of loc * 'term
| Discriminate of loc * 'term
| Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
| ElimType of loc * 'term
| Fourier of loc
| Generalize of loc * 'term * ('term, 'ident) pattern
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
- | Injection of loc * 'ident
+ | Injection of loc * 'term
| Intros of loc * int option * 'ident list
| Left of loc
| LetIn of loc * 'term * 'ident
| Split of loc
| Symmetry of loc
| Transitivity of loc * 'term
- | FwdSimpl of loc * 'ident
- | LApply of loc * 'term * ('ident * 'term) list
+ | FwdSimpl of loc * 'term
+ | LApply of loc * 'term
type thm_flavour =
[ `Definition