From 67078a0f6e58590d5a5fd835439bbf7d29bcc880 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 26 Nov 2004 23:51:30 +0000
Subject: Correction bug #879

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6357 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 35e17a07ba..dc6df2c92f 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
-- 
cgit v1.2.3