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
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =