]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_library/nCicLibrary.ml
- cic_exportation, cic_acic, acic_content (only parts related to acic)
[helm.git] / matita / components / ng_library / nCicLibrary.ml
index 7cef1e3de66fb2ad68ad2684b973527f878cb06b..8620f8cd48eca5908359cd4af95ce3c3bec47c96 100644 (file)
@@ -385,15 +385,8 @@ let get_obj u =
   with Sys_error _ ->
    try NUri.UriMap.find u !cache
    with Not_found ->
-    let ouri = NCic2OCic.ouri_of_nuri u in
-    try
-      let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
-      let l = OCic2NCic.convert_obj ouri o in
-      List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
-      HExtlib.list_last l
-    with CicEnvironment.Object_not_found u -> 
-      raise (NCicEnvironment.ObjectNotFound 
-               (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
+    raise (NCicEnvironment.ObjectNotFound 
+             (lazy (NUri.string_of_uri u)))
 ;;
 
 let clear_cache () = cache := NUri.UriMap.empty;;