type loc = CicAst.location
-type ('term, 'ident) pattern =
- ('ident * 'term) list * 'term option
+type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
type ('term, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
| Assumption of loc
| Auto of loc * int option * int option (* depth, width *)
- | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *)
+ | Change of loc * ('term,'ident) pattern * 'term
| Clear of loc * 'ident
| ClearBody of loc * 'ident
| Compare of loc * 'term
| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
+ | Fold of loc * reduction_kind * ('term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * 'term
- | Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern
+ | Generalize of loc * ('term, 'ident) pattern * 'ident option
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
| IdTac of loc
| Injection of loc * 'term