| Assumption of loc
| Auto of loc * int option * int option (* depth, width *)
| Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *)
+ | Clear of loc * 'ident
+ | ClearBody of loc * 'ident
| Compare of loc * 'term
| Constructor of loc * int
| Contradiction of loc
| ElimType of loc * 'term
| Exact of loc * 'term
| Exists of loc
- | Fold of loc * reduction_kind * 'term
+ | Fail of loc
+ | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * 'term
| Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
+ | IdTac of loc
| Injection of loc * 'term
| Intros of loc * int option * 'ident list
| LApply of loc * 'term option * 'term
| LetIn of loc * 'term * 'ident
| Reduce of loc * reduction_kind * ('term, 'ident) pattern
| Reflexivity of loc
- | Replace of loc * 'term * 'term (* what, with what *)
+ | Replace of loc * ('term, 'ident) pattern * 'term
| Rewrite of loc * direction * 'term * ('term, 'ident) pattern
| Right of loc
| Ring of loc
type ('term, 'ident) tactical =
| Tactic of loc * ('term, 'ident) tactic
- | Fail of loc
| Do of loc * int * ('term, 'ident) tactical
- | IdTac of loc
| Repeat of loc * ('term, 'ident) tactical
| Seq of loc * ('term, 'ident) tactical list (* sequential composition *)
| Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list