+ | NAuto (_,(l,flgs)) ->
+ "nauto" ^
+ (if l <> [] then (" by " ^
+ (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
+ | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
+ | NConstructor (_,None,l) -> "@ " ^
+ String.concat " " (List.map CicNotationPp.pp_term l)
+ | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
+ String.concat " " (List.map CicNotationPp.pp_term l)
+ | NCase1 (_,n) -> "*" ^ n ^ ":"
+ | NChange (_,what,wwhat) -> "nchange " ^ assert false ^
+ " with " ^ CicNotationPp.pp_term wwhat
+ | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
+ | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false