`Def (K.Const,ty,
build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
| NCic.Constant (_,_,None,ty,_) ->
let ty = nast_of_cic ~context:[] ty in
`Def (K.Const,ty,
build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
| NCic.Constant (_,_,None,ty,_) ->
let ty = nast_of_cic ~context:[] ty in