let extract_alias types uri =
fst(List.fold_left (
fun (acc,i) (name, _, _, cl) ->
- ((name, UriManager.string_of_uriref (uri,[i]))
+ (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None))
::
(fst(List.fold_left (
fun (acc,j) (name,_) ->
- (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
- ) (acc,1) cl))),i+1
+ (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i
+ (Some j))) :: acc) , j+1)
+ ) (acc,1) cl)),i+1
) ([],0) types)
let env_of_list l env =
- let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri suri) l in
+ let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in
DisambiguateTypes.env_of_list l' env
-(*
-let add_aliases_for_inductive_def status types suri =
- let uri = UriManager.uri_of_string suri in
- (* aliases for the constructors and types *)
- let aliases = env_of_list (extract_alias types uri) status.aliases in
- (* aliases for the eliminations principles *)
- let base = String.sub suri 0 (String.length suri - 4) in
- let alisases =
- env_of_list
- (List.fold_left (
- fun acc suffix ->
- if List.exists (
- fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
- ) status.objects then
- let u = base ^ suffix in
- (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
- else
- acc
- ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
- in
- {status with aliases = aliases }
-*)
-
let add_aliases_for_inductive_def status types suri =
let uri = UriManager.uri_of_string suri in
let aliases = env_of_list (extract_alias types uri) status.aliases in
[bodyuri,xmlbodypath]
| _-> assert false)
-let unregister_if_some = function
- | Some u -> Http_getter.unregister' u | None -> ()
-
let remove_object_from_disk uri path =
Sys.remove path;
Http_getter.unregister' uri