String.concat " "
(List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
| Assumption _ -> "assumption"
+ | Cases (_, term, idents) -> sprintf "cases " ^ term_pp term ^
+ pp_intros_specs (None, idents)
| Change (_, where, with_what) ->
sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
| Clear (_,ids) -> sprintf "clear %s" (pp_idents ids)
(match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
(match ident_opt with None -> "" | Some ident -> " as " ^ ident)
| Left _ -> "left"
- | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident
+ | LetIn (_, term, ident) -> sprintf "letin %s \\def %s" ident (term_pp term)
| Reduce (_, kind, pat) ->
sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
| Reflexivity _ -> "reflexivity"