Bug fixed: refreshing of uris for the db.

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index a36b70bf4a6404b6b1302eb182076b95fa71c4ea..0519e414672057cbbefed2fe1167a6b95a50b803 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -15,6 +15,22 @@ exception LibraryOutOfSync of string Lazy.t
 
 let magic = 0;;
 
+let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
+
+let rec refresh_uri_in_term =
+ function
+    NCic.Const (NReference.Ref (u,spec)) ->
+     NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
+  | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t
+;;
+
+let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) =
+ assert (metasenv = []);
+ assert (subst = []);
+ uri,height,metasenv,subst,
+  NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
+;;
+
 let path_of_baseuri ?(no_suffix=false) baseuri =
  let uri = NUri.string_of_uri baseuri in
  let path = String.sub uri 4 (String.length uri - 4) in
@@ -49,6 +65,7 @@ type timestamp =
 let time0 = [],[],NUri.UriMap.empty;;
 let storage = ref [];;
 let local_aliases = ref [];;
+
 let set_global_aliases,get_global_aliases =
  let global_aliases = ref [] in
   let store_db () =
@@ -62,7 +79,14 @@ let set_global_aliases,get_global_aliases =
 
 let init () =
  try
-  set_global_aliases (require_path (db_path ()))
+  let global_aliases = require_path (db_path ()) in
+  let global_aliases =
+   List.map
+    (fun (uri,name,NReference.Ref (uri2,spec)) ->
+      refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec
+    ) global_aliases
+  in
+   set_global_aliases global_aliases
  with
   Sys_error _ -> ()
 ;;
@@ -98,22 +122,6 @@ let serialize ~baseuri dump =
  time_travel (new status)
 ;;
 
-let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
-
-let rec refresh_uri_in_term =
- function
-    NCic.Const (NReference.Ref (u,spec)) ->
-     NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
-  | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t
-;;
-
-let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) =
- assert (metasenv = []);
- assert (subst = []);
- uri,height,metasenv,subst,
-  NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
-;;
-
 module type Serializer =
  sig
   type status