| AutoBatch (_,params) -> "autobatch " ^
pp_auto_params ~term_pp params
| Assumption _ -> "assumption"
- | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
- pp_tactic_pattern pattern ^
- pp_intros_specs "names " specs
+ | Cases (_, term, pattern, specs) ->
+ Printf.sprintf "cases %s %s%s"
+ (term_pp term)
+ (pp_tactic_pattern pattern)
+ (pp_intros_specs "names " specs)
| Change (_, where, with_what) ->
Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
| Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)