...

[helm.git] / helm / software / components / ng_kernel / nCicLibrary.ml

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 6d1797677a6f23b8c587afe71709990f9e4189b1..e7d7c3b11d21a71b677713a5725801995f299ef0 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -23,6 +23,9 @@ let refresh_uri_in_universe =
 
 let rec refresh_uri_in_term =
  function
+  | NCic.Meta (i,(n,NCic.Ctx l)) ->
+     NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l)))
+  | NCic.Meta _ as t -> t
   | NCic.Const (NReference.Ref (u,spec)) ->
      NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
   | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l))
@@ -71,7 +74,7 @@ let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
 
 type timestamp =
  [ `Obj of NUri.uri * NCic.obj 
- | `Constr of bool * NCic.universe * NCic.universe] list *
+ | `Constr of NCic.universe * NCic.universe] list *
  (NUri.uri * string * NReference.reference) list *
  NCic.obj NUri.UriMap.t *
  NUri.uri list
@@ -140,6 +143,10 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
+class type g_status =
+ object
+  method timestamp: timestamp
+ end
 
 class status =
  object
@@ -147,7 +154,7 @@ class status =
   method timestamp = timestamp
   method set_timestamp v = {< timestamp = v >}
   method set_library_status
-   : 'status. < timestamp : timestamp; .. > as 'status -> 'self
+   : 'status. #g_status as 'status -> 'self
    = fun o -> {< timestamp = o#timestamp >}
  end
 
@@ -200,12 +207,13 @@ module Serializer(S: sig type status end) =
   let register tag require =
    assert (not (List.mem tag !already_registered));
    already_registered := tag :: !already_registered;
+   let old_require1 = !require1 in
    require1 :=
-    (fun (tag',data) as x ->
-     if tag=tag' then
-      require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term 
-     else
-      !require1 x);
+     (fun (tag',data) as x ->
+      if tag=tag' then
+       require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term 
+      else
+       old_require1 x);
    (fun x -> tag,Obj.repr x)
 
   let serialize = serialize
@@ -262,12 +270,9 @@ let resolve name =
 ;;
 
 let aliases_of uri =
- try
   HExtlib.filter_map
    (fun (uri',_,nref) ->
      if NUri.eq uri' uri then Some nref else None) !local_aliases
- with
-  Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
 ;;
 
 let add_obj status ((u,_,_,_,_) as obj) =
@@ -305,9 +310,9 @@ let add_obj status ((u,_,_,_,_) as obj) =
   status#set_timestamp (!storage,!local_aliases,!cache,!includes)
 ;;
 
-let add_constraint status strict u1 u2 = 
-  NCicEnvironment.add_constraint strict u1 u2;
-  storage := (`Constr (strict,u1,u2)) :: !storage;
+let add_constraint status u1 u2 = 
+  NCicEnvironment.add_lt_constraint u1 u2;
+  storage := (`Constr (u1,u2)) :: !storage;
   status#set_timestamp (!storage,!local_aliases,!cache,!includes)
 ;;