X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=24217d6aea2628229ab3718dcf521ce267c4db4e;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=6871dc6ee3775ba4983f88f48ac5757c59ed6ec1;hpb=750305d95b8f6bb40b5be0e9dfd05d42b256f2a1;p=helm.git

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index 6871dc6ee..24217d6ae 100644
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -1329,7 +1329,7 @@ let typecheck_obj status (uri,height,metasenv,subst,kind) =
              (guarded_by_constructors status ~subst ~metasenv types bo r_uri r_len len)
              then
                raise (TypeCheckerFailure
-                (lazy "CoFix: not guarded by constructors"))
+                (lazy ("CoFix: not guarded by constructors: " ^ status#ppobj (uri,height,metasenv,subst,kind))))
         ) fl dfl
 ;;
 
@@ -1376,7 +1376,7 @@ let _ = NCicReduction.set_get_relevance get_relevance;;
 
 let indent = ref 0;;
 let debug = true;;
-let logger =
+let _logger =
     let do_indent () = String.make !indent ' ' in  
     (function 
       | `Start_type_checking s ->