- sprintf "fold %s %s %s" (pp_reduction_kind kind) (pp_term_ast term)
- (pp_pattern pattern)
- | Generalize (_, term, ident, pattern) ->
- sprintf "generalize %s%s %s" (pp_term_ast term)
+ sprintf "fold %s %s %s" (pp_reduction_kind kind)
+ (pp_term_ast term) (pp_pattern pattern)
+ | FwdSimpl (_, hyp, idents) ->
+ sprintf "fwd %s%s" hyp
+ (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+ | Generalize (_, pattern, ident) ->
+ sprintf "generalize %s%s" (pp_pattern pattern)