]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/oCicTypeChecker.ml
transformation almost finisced, not tested
[helm.git] / helm / software / components / ng_kernel / oCicTypeChecker.ml
index 2139654c7bd47280d155fa40c23cd2c2825898b1..878706b9effb106430a71000f1995c5d4a68d384 100644 (file)
@@ -1,7 +1,7 @@
 
 let typecheck_obj uri obj =
   try 
-    NCicTypeChecker.typecheck_obj (OCic2NCic.convert_obj uri obj); true
+    NCicTypeChecker.typecheck_obj (fst (OCic2NCic.convert_obj uri obj)); true
   with 
     | NCicTypeChecker.TypeCheckerFailure _
     | NCicTypeChecker.AssertFailure _ -> false