| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
- | NConstructor (_,None) -> "@"
- | NConstructor (_,Some x) -> "@" ^ string_of_int x
+ | 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