| DecideEquality of loc
| Decompose of loc * 'term
| Discriminate of loc * 'term
- | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
- | ElimType of loc * 'term
+ | Elim of loc * 'term * 'term option * int option * 'ident list
+ | ElimType of loc * 'term * 'term option * int option * 'ident list
| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * reduction_kind * ('term, 'ident) pattern
+ | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
| Fourier of loc
- | FwdSimpl of loc * 'term
+ | FwdSimpl of loc * string * 'ident list
| 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
| Intros of loc * int option * 'ident list
- | LApply of loc * 'term option * 'term * 'ident option
+ | LApply of loc * int option * 'term list * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
| Reduce of loc * reduction_kind * ('term, 'ident) pattern
(string * CicAst.term) list
type ('term,'obj) command =
+ | Default of loc * string * UriManager.uri list
+ | Include of loc * string
| Set of loc * string * string
| Drop of loc
| Qed 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
- | Tries of loc * ('term, 'ident) tactical list
+ | First of loc * ('term, 'ident) tactical list
(* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
| Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
+ | Solve of loc * ('term, 'ident) tactical list
type ('term, 'obj, 'ident) code =