let pp_nmacro = function
| NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term)
+ | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
;;
let pp_macro ~term_pp ~lazy_term_pp =
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NInverter (_,_,_,_,_)
| NObj (_,_)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"