From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 6 Apr 2009 15:35:59 +0000 (+0000)
Subject: better error message
X-Git-Tag: make_still_working~4116
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a029c5b4927384b23935fceeda7e05ba8f57f3f;p=helm.git

better error message
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index a4ff68d9f..3459c8dd2 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -375,7 +375,9 @@ let rec typeof ~subst ~metasenv context term =
          match List.nth context (n - 1) with
          | (_,C.Decl ty) -> S.lift n ty
          | (_,C.Def (_,ty)) -> S.lift n ty
-        with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")))
+        with Failure _ -> 
+          raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
+            ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
     | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
     | C.Sort (C.Type _) -> 
         raise (AssertFailure (lazy ("Cannot type an inferred type: "^