diff options
| -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 |