*)
type direction = [ `LeftToRight | `RightToLeft ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
+type 'term reduction_kind =
+ [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
type loc = CicNotationPt.location
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
| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
+ | Fold of loc * 'term reduction_kind * 'term * ('term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * string * 'ident list
| Generalize of loc * ('term, 'ident) pattern * '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
+ | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern
| Reflexivity of loc
| Replace of loc * ('term, 'ident) pattern * 'term
| Rewrite of loc * direction * 'term * ('term, 'ident) pattern
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
| Obj of loc * 'obj
- | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
- CicNotationPt.term
- (* level 1 pattern, associativity, precedence, level 2 pattern *)
+ | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
+ int * CicNotationPt.term
+ (* direction, l1 pattern, associativity, precedence, l2 pattern *)
| Interpretation of loc *
string * (string * CicNotationPt.argument_pattern list) *
CicNotationPt.cic_appl_pattern