- | _,_,_,_,NCic.Constant (rel, name, Some bo, ty, _) ->
- Cic.Constant (name, Some (convert_term 0 bo), convert_term 0 ty, [],[])
- | _,_,_,_,NCic.Constant (rel, name, None, ty, _) ->
- Cic.Constant (name, None, convert_term 0 ty, [],[])
- | _,_,_,_,NCic.Fixpoint (is_fix, fl, _) ->
- Cic.Constant ("pippo", Some (convert_fix 0 fl),
- convert_term 0 (let _,_,_,ty,_ = List.hd fl in ty), [], [])
- | _,_,_,_,NCic.Inductive _ -> assert false
+ | u,_,_,_,NCic.Constant (_, name, Some bo, ty, _) ->
+ [ouri_of_nuri u,Cic.Constant
+ (name, Some (convert_term u 0 bo), convert_term u 0 ty, [],[])]
+ | u,_,_,_,NCic.Constant (_, name, None, ty, _) ->
+ [ouri_of_nuri u,Cic.Constant (name, None, convert_term u 0 ty, [],[])]
+ | u,_,_,_,NCic.Fixpoint (is_fix, fl, _) ->
+ 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,[])]