-(* | Named_intros of loc * 'ident list (* joined with Intros above *) *)
-(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
- | ReduceAt of loc * reduction_kind * 'ident * 'term
- | 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 *)