| DecideEquality of loc
| 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
+ | Elim of loc * 'term * 'term option * int option * 'ident list
+ | ElimType of loc * 'term * 'term option * int option * 'ident list
| Exact of loc * 'term
| Exists of loc
| Fail of loc