X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=ef3bca22d06941ebfa20fe883d4423eb7ec87e0e;hb=235d5cc96af46d0406bdd28222f56b3ee2bf827e;hp=4d60e5d42948f4729d2d0fef14e951c65985f554;hpb=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 4d60e5d42..ef3bca22d 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -19,6 +19,9 @@ exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
 exception BadConstraint of string Lazy.t;;
 
+let get_obj = ref (fun _ -> assert false);;
+let set_get_obj f = get_obj := f;;
+
 let type0 = []
 
 let max l1 l2 =
@@ -29,16 +32,6 @@ let max l1 l2 =
 
 let le_constraints = ref [] (* strict,a,b *)
 
-let resolve_universe u =
-  HExtlib.list_findopt 
-    (fun (_,a,b) _ -> 
-      prerr_endline (NUri.name_of_uri a);
-           if NUri.name_of_uri a = u then Some a 
-      else if NUri.name_of_uri b = u then Some b
-      else None) 
-    !le_constraints
-;;
-
 let rec le_path_uri avoid strict a b =
  (not strict && NUri.eq a b) ||
  List.exists
@@ -135,17 +128,13 @@ let get_checked_obj u =
     Not_found ->
      let saved_frozen_list = !frozen_list in
      try
-      let obj =
-       try NCicLibrary.get_obj u
-       with
-        NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m)
-      in
-        frozen_list := (u,obj)::saved_frozen_list;
-        !typecheck_obj obj;
-        frozen_list := saved_frozen_list;
-        let obj = `WellTyped obj in
-        NUri.UriHash.add cache u obj;
-        obj
+      let obj = !get_obj u in
+       frozen_list := (u,obj)::saved_frozen_list;
+       !typecheck_obj obj;
+       frozen_list := saved_frozen_list;
+       let obj = `WellTyped obj in
+       NUri.UriHash.add cache u obj;
+       obj
      with
         Sys.Break as e ->
          frozen_list := saved_frozen_list;