From 7a029c5b4927384b23935fceeda7e05ba8f57f3f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2009 15:35:59 +0000 Subject: [PATCH] better error message --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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: "^ -- 2.39.2