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

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index fb733cdfc..e7d7c3b11 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -74,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
@@ -270,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) =
@@ -313,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)
 ;;