diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
| commit | 6497f27021fec4e01f2182014f2bb1989b4707f9 (patch) | |
| tree | 473be7e63895a42966970ab6a70998113bc1bd59 /pretyping/evarconv.ml | |
| parent | 6b649aba925b6f7462da07599fe67ebb12a3460e (diff) | |
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6f396b43..0ee95a0f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml,v 1.44.6.1 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: evarconv.ml,v 1.44.6.2 2004/11/26 23:51:39 herbelin Exp $ *) open Util open Names @@ -39,8 +39,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 |