- | Contradiction
- | Cut of 'term
- | Decompose of 'ident * 'ident list (* where, which principles *)
- | Discriminate of 'ident
- | Elim of 'term * 'term option (* what to elim, which principle to use *)
- | ElimType of 'term
- | Exact of 'term
- | Exists
- | Fold of reduction_kind * 'term
- | Fourier
- | Injection of 'ident
- | Intros of int option * 'ident list
- | Left
- | LetIn of 'term * 'ident
-(* | Named_intros of 'ident list (* joined with Intros above *) *)
- | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *)
- | Reflexivity
- | Replace of 'term * 'term (* what, with what *)
- | Replace_pattern of 'term pattern * 'term
- | Rewrite of direction * 'term * 'ident option
- | Right
- | Ring
- | Split
- | Symmetry
- | Transitivity of 'term
+ | Contradiction of loc
+ | Cut of loc * 'term
+ | Decompose of loc * 'ident * 'ident list (* where, which principles *)
+ | Discriminate of loc * 'ident
+ | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
+ | ElimType of loc * 'term
+ | Exact of loc * 'term
+ | Exists of loc
+ | Fold of loc * reduction_kind * 'term
+ | Fourier of loc
+ | Goal of loc * int (* change current goal, argument is goal number 1-based *)
+ | Hint of loc
+ | Injection of loc * 'ident
+ | Intros of loc * int option * 'ident list
+ | Left of loc
+ | LetIn of loc * 'term * 'ident
+(* | Named_intros of loc * 'ident list (* joined with Intros above *) *)
+(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
+ | Reduce of loc * reduction_kind * ('term list * 'term pattern) option
+ (* kind, (what, where)
+ * if second argument is None, reduction is applied to the current goal,
+ * otherwise to each occurrence of loc * terms given in list occuring in term
+ * pattern *)
+ | Reflexivity of loc
+ | Replace of loc * 'term * 'term (* what, with what *)
+ | Replace_pattern of loc * 'term pattern * 'term
+ | Rewrite of loc * direction * 'term * 'ident option
+ | Right of loc
+ | Ring of loc
+ | Split of loc
+ | Symmetry of loc
+ | Transitivity of loc * 'term