- Cic.Constant (UriManager.name_of_uri (NUri.ouri_of_nuri u),
- Some (convert_fix is_fix u 0 fl),
- convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], [])
- | _,_,_,_,NCic.Inductive _ -> assert false
+ List.map
+ (fun nth ->
+ let name =
+ UriManager.name_of_uri (ouri_of_nuri u) ^ string_of_int nth in
+ let buri = UriManager.buri_of_uri (ouri_of_nuri u) in
+ let uri = UriManager.uri_of_string (buri ^"/"^name^".con") in
+ uri,
+ Cic.Constant (name,
+ Some (convert_fix is_fix u nth fl),
+ convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], []))
+ (let rec seq = function 0 -> [0]|n -> n::seq (n-1) in
+ seq (List.length fl-1))
+ | u,_,_,_,NCic.Inductive (inductive,leftno,itl,_) ->
+ let itl =
+ List.map
+ (function (_,name,ty,cl) ->
+ let cl=List.map (function (_,name,ty) -> name,convert_term u 0 ty) cl in
+ name,inductive,convert_term u 0 ty,cl
+ ) itl
+ in
+ [ouri_of_nuri u, Cic.InductiveDefinition (itl,[],leftno,[])]