type note = string
type where = (name * name) option
type inferred = Cic.annterm
+type pattern = Cic.annterm
type step = Note of note
| Theorem of name * what * note
| Intros of count option * name list * note
| Cut of name * what * note
| LetIn of name * what * note
- | Rewrite of how * what * where * note
- | Elim of what * using option * note
+ | Rewrite of how * what * where * pattern * note
+ | Elim of what * using option * pattern * note
| Apply of what * note
- | Change of inferred * what * where * note
+ | Change of inferred * what * where * pattern * note
| ClearBody of name * note
| Branch of step list list * note