pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NSmartApply (_,t) -> "fixme"
| NAuto (_,(None,flgs)) ->
- "nauto" ^
+ "nautobatch" ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NAuto (_,(Some l,flgs)) ->
- "nauto" ^ " by " ^
+ "nautobatch" ^ " by " ^
(String.concat "," (List.map CicNotationPp.pp_term l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
| NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
| NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
- | NDestruct _ -> "ndestruct"
+ | NDestruct (_,dom,skip) -> "ndestruct ..."
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
(term_pp t) arity saturations
(if do_composites then "" else "nocomposites")
-let pp_ncommand = function
+let pp_ncommand ~obj_pp = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
| NDiscriminator (_,_)
| NInverter (_,_,_,_,_)
- | NObj (_,_)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
+ | NObj (_,obj) -> obj_pp obj
| NQed (_) -> "nqed"
| NCopy (_,name,uri,map) ->
"copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
pp_non_punctuation_tactical tac
^ pp_punctuation_tactical punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
- | NCommand (_, cmd) -> pp_ncommand cmd ^ "."
+ | NCommand (_, cmd) ->
+ let obj_pp = Obj.magic obj_pp in
+ pp_ncommand ~obj_pp cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
function