diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-26 23:51:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-26 23:51:30 +0000 |
| commit | 67078a0f6e58590d5a5fd835439bbf7d29bcc880 (patch) | |
| tree | 6b76ece1b9c423444c2257aea9d5ddfac11293d6 | |
| parent | 7c92f6e260c30057b0505c5a79456d20222f818d (diff) | |
Correction bug #879
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6357 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 35e17a07b..dc6df2c92 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -40,8 +40,11 @@ let flex_kind_of_term c l = let eval_flexible_term env c = match kind_of_term c with | Const c -> constant_opt_value env c - | Rel n -> let (_,v,_) = lookup_rel n env in option_app (lift n) v - | Var id -> let (_,v,_) = lookup_named id env in v + | Rel n -> + (try let (_,v,_) = lookup_rel n env in option_app (lift n) v + with Not_found -> None) + | Var id -> + (try let (_,v,_) = lookup_named id env in v with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) | Lambda _ -> Some c | _ -> assert false |