-let rec pp_tactic ~term_pp ~lazy_term_pp =
- let pp_reduction_kind = pp_reduction_kind ~term_pp in
- let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
+let pp_ntactic ~map_unicode_to_tex = function
+ | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
+ | NCase1 (_,n) -> "*" ^ n ^ ":"
+ | NChange (_,what,wwhat) -> "nchange " ^ assert false ^
+ " with " ^ CicNotationPp.pp_term wwhat
+ | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
+ | NId _ -> "nid"
+ | NIntro (_,n) -> "#" ^ n
+ | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
+ | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false
+;;
+
+let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
+ let pp_terms = pp_terms ~term_pp in
+ let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
+ let pp_reduction_kind = pp_reduction_kind ~term_pp in
+ let pp_tactic_pattern =
+ pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
+ let rec pp_tactic =