| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * reduction_kind * ('term, 'ident) pattern
+ | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * string * 'ident list
| Generalize of loc * ('term, 'ident) pattern * 'ident option
(string * CicAst.term) list
type ('term,'obj) command =
+ | Include of loc * string
| Set of loc * string * string
| Drop of loc
| Qed of loc