*)
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
| 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 * int *
- 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