| Type of UriManager.uri * int
type 'lazy_term reduction =
- [ `Demodulate
- | `Normalize
+ [ `Normalize
| `Reduce
| `Simpl
| `Unfold of 'lazy_term option
| Contradiction of loc
| Cut of loc * 'ident option * 'term
| Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
+ | Demodulate of loc
| Discriminate of loc * 'term
| Elim of loc * 'term * 'term option * int option * 'ident list
| ElimType of loc * 'term * 'term option * int option * 'ident list