Error reporting improved.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5c3dc08f1dc33c61cec2e09e34e8f5ef86ed51f5..cea5a277218213cbc09da878b4256899e2f5ae8b 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -981,7 +981,14 @@ and type_of_aux' env t =
   let module S = CicSubstitution in
   let module U = UriManager in
    function
-      C.Rel n -> S.lift n (List.nth env (n - 1))
+      C.Rel n ->
+       let t =
+        try
+         List.nth env (n - 1)
+        with
+         _ -> raise (NotWellTyped "Not a close term")
+       in
+        S.lift n t
     | C.Var uri ->
       incr fdebug ;
       let ty = type_of_variable uri in