| ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
| AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
| RewritingStep of
- loc * 'term option * 'term *
- [ `Term of 'term | `Auto of (string * string) list ] * Cic.name option
+ loc * (string option * 'term) option * 'term *
+ [ `Term of 'term | `Auto of (string * string) list ] *
+ bool (* last step*)
type search_kind = [ `Locate | `Hint | `Match | `Elim ]