let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri 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
val add_obj:
UriManager.uri -> Cic.obj -> MatitaTypes.status -> MatitaTypes.status
-(*
-val add_inductive_def:
- uri:UriManager.uri ->
- types:Cic.inductiveType list ->
- ?params:UriManager.uri list -> ?leftno:int -> ?attrs:Cic.attribute list ->
- ugraph:CicUniv.universe_graph ->
- MatitaTypes.status -> MatitaTypes.status
-
-val add_record_def:
- CicRecord.record_spec ->
- MatitaTypes.status -> MatitaTypes.status
-*)
-
val time_travel:
present:MatitaTypes.status -> past:MatitaTypes.status -> unit