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 (* 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 * string * 'ident list
| Generalize of loc * ('term, 'ident) pattern * 'ident option
| Symmetry of loc
| Transitivity of loc * 'term
-type thm_flavour =
- [ `Definition
- | `Fact
- | `Lemma
- | `Remark
- | `Theorem
- ]
+type thm_flavour = Cic.object_flavour
(** <name, inductive/coinductive, type, constructor list>
* true means inductive, false coinductive *)
(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 =