From d5c15e8836c2225fceaf7f2abc564b04dec653ee Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Mar 2013 23:59:51 +0000
Subject: 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
---
 interp/implicit_quantifiers.ml | 23 ++++++++---------------
 1 file changed, 8 insertions(+), 15 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 480b6a18e6..955ad9a88e 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. *)
 
-- 
cgit v1.2.3