- ng_kernel: we print the offending term when guarded_by_constructors fails

[helm.git] / matita / components / ng_kernel / nCicTypeChecker.ml

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index 6871dc6ee3775ba4983f88f48ac5757c59ed6ec1..b60734508b46b5a6fe5687086ce7a8e45bfd640c 100644 (file)
--- 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
 ;;