diff options
| -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. *) |