- 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

1 files changed, 7 insertions, 12 deletions

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