diff options
| author | delahaye | 2000-06-28 14:31:48 +0000 |
|---|---|---|
| committer | delahaye | 2000-06-28 14:31:48 +0000 |
| commit | 603111ab1d61d87640222dec37e02199f2f8cb52 (patch) | |
| tree | 04e52cc6b14768a7a528cb9672f45f1070dcf3ab | |
| parent | 1bae9189f92f394ab891f6398d94a6f58c7b47ef (diff) | |
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
| -rw-r--r-- | pretyping/typing.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |