* http://helm.cs.unibo.it/
*)
-type direction = [ `Left | `Right ]
+type direction = [ `LeftToRight | `RightToLeft ]
type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
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
- | Auto of loc * int option
| Assumption of loc
- | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *)
+ | Auto of loc * int option * int option (* depth, width *)
+ | Change of loc * ('term,'ident) pattern * 'term
+ | Clear of loc * 'ident
+ | ClearBody of loc * 'ident
| Compare of loc * 'term
| Constructor of loc * int
| Contradiction of loc
- | Cut of loc * 'term
+ | Cut of loc * 'ident option * 'term
| 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
- | 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 * ('term, 'ident) pattern
+ | 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
+ | 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
| 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
(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
(** name.
* Name is needed when theorem was started without providing a name
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
- | 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 =