From e66ba651bdd283dd490453f9d48b226730444726 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 10 May 2009 18:11:16 +0000
Subject: - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it  
 revealed a too strict test for detection of inferable metas in   Clenv.
 Restored tolerance for unbound names in interactive tactic use. - Moral
 removals of some captures of Not_found in Environ.evaluable_* since   kernel
 is assumed to deal with existing names.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.ml | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e0f364f2ee..de833c540e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -44,12 +44,9 @@ let lookup_rel n env =
   lookup_rel n env.env_rel_context
 
 let evaluable_rel n env =
-  try
-    match lookup_rel n env with
-        (_,Some _,_) -> true
-      | _ -> false
-  with Not_found -> 
-    false
+  match lookup_rel n env with
+  | (_,Some _,_) -> true
+  | _ -> false
 
 let nb_rel env = env.env_nb_rel
 
@@ -111,11 +108,9 @@ let named_body id env =
   let (_,b,_) = lookup_named id env in b
 
 let evaluable_named id env =
-  try 
-    match named_body id env with
-    |Some _      -> true
-    | _          -> false
-  with Not_found -> false
+  match named_body id env with
+  | Some _      -> true
+  | _          -> false
       
 let reset_with_named_context (ctxt,ctxtv) env =
   { env with
@@ -175,7 +170,7 @@ let constant_opt_value env cst =
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
   try let _  = constant_value env cst in true
-  with Not_found | NotEvaluableConst _ -> false
+  with NotEvaluableConst _ -> false
 
 (* Mutual Inductives *)
 let lookup_mind = lookup_mind
-- 
cgit v1.2.3