X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCicTypeChecker.ml;h=396144a5d3c9b499dd7fb6829e282292e5a0a16b;hb=e457ababc4cb5b75540cfa131a30fdee3f9bc0ed;hp=878706b9effb106430a71000f1995c5d4a68d384;hpb=b7535cd20248c564e942cc4e9058d34fbb062c6f;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.ml b/helm/software/components/ng_kernel/oCicTypeChecker.ml
index 878706b9e..396144a5d 100644
--- a/helm/software/components/ng_kernel/oCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/oCicTypeChecker.ml
@@ -1,7 +1,8 @@
 
 let typecheck_obj uri obj =
   try 
-    NCicTypeChecker.typecheck_obj (fst (OCic2NCic.convert_obj uri obj)); true
+    NCicTypeChecker.typecheck_obj (HExtlib.list_last (OCic2NCic.convert_obj uri
+    obj)); true
   with 
     | NCicTypeChecker.TypeCheckerFailure _
     | NCicTypeChecker.AssertFailure _ -> false