X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=e7d7c3b11d21a71b677713a5725801995f299ef0;hb=7b112b0cd39c5ab0db5c28636c0a7f7e36b4d6e2;hp=33276cc3df689942cd19391af7e2c30d92647d1c;hpb=a04fc65f5bbe94395cdf4397c6f9682457f4e9cd;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 33276cc3d..e7d7c3b11 100644
--- 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
 
@@ -263,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) =
@@ -306,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)
 ;;