| LetIn of loc * 'term * 'ident
| Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern
| Reflexivity of loc
+ | Rename of loc * 'ident list * 'ident list
| Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
| Rewrite of loc * direction * 'term *
- ('term, 'lazy_term, 'ident) pattern
+ ('term, 'lazy_term, 'ident) pattern * 'ident list
| Right of loc
| Ring of loc
| Split of loc