diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:51 +0000 |
commit | d5c15e8836c2225fceaf7f2abc564b04dec653ee (patch) | |
tree | 35018179dc402dc961de2fa60d14abbe5d192e11 | |
parent | 69b2a2dddad32ccc8dc4a1bad707101e768f4f32 (diff) |
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
-rw-r--r-- | interp/implicit_quantifiers.ml | 23 |
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. *) |