From 603111ab1d61d87640222dec37e02199f2f8cb52 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 28 Jun 2000 14:31:48 +0000
Subject: Rattrapage d'un Not_found pour les VAR's.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@519 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typing.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 873939c91d..0fbe3c7587 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,7 +35,10 @@ let rec execute mf env sigma cstr =
 	relative env n
 
     | IsVar id -> 
-	make_judge cstr (snd (lookup_var id env))
+      (try
+         make_judge cstr (snd (lookup_var id env))
+       with Not_found ->
+         error ("execute: variable " ^ (string_of_id id) ^ " not defined"))
 	  
     | IsAbst _ ->
         if evaluable_abst env cstr then 
-- 
cgit v1.2.3