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