]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicEnvironment.ml
...
[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.ml
index 8d0ae1a4f9e7e1a86225a23f2e5866fee1b8e3c0..02b3baab68e414f102277ea362d68df17323e4db 100644 (file)
@@ -7,7 +7,8 @@ let get_checked_obj u =
     let o,_ = 
       CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph 
         ouri in
-    let no,_ = OCic2NCic.convert_obj ouri o in
+    (* FIX: add all objects to the environment and give back the last one *)
+    let no = HExtlib.list_last (OCic2NCic.convert_obj ouri o) in
     NUri.UriHash.add cache u no;
     no
 ;;