| _ -> [uri]
let add_obj refinement_toolkit uri obj status =
- let baseuri, status = GrafiteTypes.get_baseuri status in
let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
let add_to_universe (universe,status) uri =
let term = CicUtil.term_of_uri uri in
List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
List.iter LibrarySync.remove_obj objs_to_remove
-let init () =
+let init baseuri =
LibrarySync.remove_all_coercions ();
LibraryObjects.reset_defaults ();
{
objects = [];
coercions = [];
universe = Universe.empty;
- baseuri = None;
+ baseuri = baseuri;
}