let innertypesuri = UriManager.innertypesuri_of_uri uri in
Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
Http_getter.register' innertypesuri
- (Helm_registry.get "annotations.url" ^
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri innertypesuri) ^ ".xml"
) ;
(* constant type / variable / mutual inductive types definition *)
Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
Http_getter.register' uri
- (Helm_registry.get "annotations.url" ^
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri uri) ^ ".xml"
) ;
in
Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
Http_getter.register' bodyuri
- (Helm_registry.get "annotations.url" ^
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri bodyuri) ^ ".xml"
)
exception WrongProof;;
let pathname_of_annuri uristring =
- Helm_registry.get "annotations.dir" ^
+ Helm_registry.get "local_library.dir" ^
Str.replace_first (Str.regexp "^cic:") "" uristring
;;