+ let ctx,_ = split_kind_prods [] arity in
+ let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
+ let ref =
+ NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
+ let status =
+ status#set_extraction_db
+ (ReferenceMap.add ref (ctx,None) status#extraction_db) in
+ let cl =
+ HExtlib.list_mapi
+ (fun (_,_,ty) j ->
+ let ctx,ty =
+ NCicReduction.split_prods status ~subst:[] [] leftno ty in
+ let ty = typ_of status ~metasenv ctx ty in
+ NReference.mk_constructor (j+1) ref,ty
+ ) cl
+ in
+ status,i+1,(ref,left,right,cl)::res
+ ) (status,0,[]) il