type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
+type ('term, 'ident) type_spec =
+ | Ident of 'ident
+ | Type of UriManager.uri * int
+
type ('term, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
| Assumption of loc
- | Auto of loc * int option * int option (* depth, width *)
+ | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *)
| Change of loc * ('term,'ident) pattern * 'term
| Clear of loc * 'ident
| ClearBody of loc * 'ident
| Contradiction of loc
| Cut of loc * 'ident option * 'term
| DecideEquality of loc
- | Decompose of loc * 'term
+ | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
| Discriminate of loc * 'term
| Elim of loc * 'term * 'term option * int option * 'ident list
| ElimType of loc * 'term * 'term option * int option * 'ident list