Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16279 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 15 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 480b6a18e..955ad9a88 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -69,24 +69,17 @@ let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_tab
 let ids_of_list l =
   List.fold_right Id.Set.add l Id.Set.empty
 
-let locate_reference qid =
-  match Nametab.locate_extended qid with
-    | TrueGlobal ref -> true
-    | SynDef kn -> true
-
 let is_global id =
-  try
-    locate_reference (qualid_of_ident id)
-  with Not_found ->
-    false
+  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
+  with Not_found -> false
+
+let is_named id env =
+  try ignore (Environ.lookup_named id env); true
+  with Not_found -> false
 
 let is_freevar ids env x =
-  try
-    if Id.Set.mem x ids then false
-    else
-      try ignore(Environ.lookup_named x env) ; false
-      with _ -> not (is_global x)
-  with _ -> true
+  not (Id.Set.mem x ids || is_named x env || is_global x)
+
 
 (* Auxiliary functions for the inference of implicitly quantified variables. *)