...

[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 fb733cdfcb877366658881b96c2365f06b37352a..e7d7c3b11d21a71b677713a5725801995f299ef0 100644 (file)
--- 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)
 ;;