let command_terminator = tactical_terminator
let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
let command_terminator = tactical_terminator
let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
pp_intros_specs (None, idents)
| Change (_, where, with_what) ->
Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
pp_intros_specs (None, idents)
| 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_idents ids)
- | ClearBody (_,id) -> Printf.sprintf "clearbody %s" id
+ | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
+ | ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id])
| Constructor (_,n) -> "constructor " ^ string_of_int n
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
| Constructor (_,n) -> "constructor " ^ string_of_int n
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
function
| Note (_,"") -> Printf.sprintf "\n"
let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
function
| Note (_,"") -> Printf.sprintf "\n"