From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2001 11:01:08 +0000 (+0000)
Subject: Error reporting improved.
X-Git-Tag: mlminidom_0_2_2~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fc655b91976612bc3b2650f1e463f98208a8b804;p=helm.git

Error reporting improved.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5c3dc08f1..cea5a2772 100644
--- 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