- 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, 3 insertions, 3 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 576e217aa5..dd2af306c9 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -231,9 +231,9 @@ let clenv_dependent hyps_only clenv =
   let nonlinear = duplicated_metas (clenv_value clenv) in
   (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
-    (fun mv -> (Metaset.mem mv deps &&
-                not (hyps_only && Metaset.mem mv ctyp_mvs))
-               or List.mem mv nonlinear) 
+    (fun mv -> if Metaset.mem mv deps
+               then not (hyps_only && Metaset.mem mv ctyp_mvs)
+               else List.mem mv nonlinear)
     mvs
 
 let clenv_missing ce = clenv_dependent true ce