- | 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
- | Hint
- | 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 *) *)
- | Reduce of reduction_kind * ('term list * 'term pattern) option
+ | 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