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

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index 0a73358e0..24217d6ae 100644
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -186,7 +186,7 @@ let does_not_occur status ~subst context n nn t =
     | C.Rel m when m <= k || m > nn+k -> ()
     | C.Rel m ->
         (try match List.nth context (m-1-k) with
-          | _,C.Def (bo,_) -> aux (n-m) () bo
+          | _,C.Def (bo,_) -> aux 0 () (S.lift status (m-k) bo)
           | _ -> ()
          with Failure _ -> assert false)
     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
@@ -391,7 +391,7 @@ let rec typeof (status:#NCic.status) ~subst ~metasenv context term =
          match List.nth context (n - 1) with
          | (_,C.Decl ty) -> S.lift status n ty
          | (_,C.Def (_,ty)) -> S.lift status n ty
-        with Failure _ -> 
+        with Failure _ | Invalid_argument _ -> 
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ status#ppcontext ~metasenv ~subst context))))
     | C.Sort s -> 
@@ -698,15 +698,16 @@ and eat_prods status ~subst ~metasenv context he ty_he args_with_ty =
           if R.are_convertible status ~metasenv ~subst context ty_arg s then
             aux (S.subst status ~avoid_beta_redexes:true arg t) tl
           else
+           let indent s = "   " ^ (Str.global_replace (Str.regexp "\n") "\n   " s) in
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong application of %s: the argument %s has type"^^
+                  ("Appl: wrong application of\n%s\nThe argument\n%s\nhas type"^^
                    "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
-                  (status#ppterm ~subst ~metasenv ~context he)
-                  (status#ppterm ~subst ~metasenv ~context arg)
-                  (status#ppterm ~subst ~metasenv ~context ty_arg)
-                  (status#ppterm ~subst ~metasenv ~context s)
+                  (indent (status#ppterm ~subst ~metasenv ~context he))
+                  (indent (status#ppterm ~subst ~metasenv ~context arg))
+                  (indent (status#ppterm ~subst ~metasenv ~context ty_arg))
+                  (indent (status#ppterm ~subst ~metasenv ~context s))
                   (status#ppcontext ~subst ~metasenv context))))
        | _ ->
           raise 
@@ -1130,7 +1131,7 @@ and get_relevance status ~metasenv ~subst context t args =
               | C.Sort C.Prop ->
                   false::(aux context new_ty tl)
               | C.Sort _
-                   | C.Meta _ -> true::(aux context new_ty tl)
+              | C.Meta _ -> true::(aux context new_ty tl)
               | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
                      "Prod: the type %s of the source of %s is not a sort" 
                       (status#ppterm ~subst ~metasenv ~context sort)
@@ -1328,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
 ;;
 
@@ -1375,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 ->