- | C.Appl (C.MutConstruct _ as he::tl) ->
- let hes = pp he context in
- let stl = String.concat "," (clean_args context tl) in
+ | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
+ let nparams =
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (_,_,nparams,_) -> nparams
+ | _ -> assert false in
+ let hes = pp ~in_type he context in
+ let stl = String.concat "," (clean_args nparams context tl) in