diff options
Diffstat (limited to 'vernac/search.ml')
| -rw-r--r-- | vernac/search.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/vernac/search.ml b/vernac/search.ml index a2a4fb40..e8ccec11 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -22,8 +22,8 @@ open Nametab module NamedDecl = Context.Named.Declaration -type filter_function = global_reference -> env -> constr -> bool -type display_function = global_reference -> env -> constr -> unit +type filter_function = GlobRef.t -> env -> constr -> bool +type display_function = GlobRef.t -> env -> constr -> unit (* This option restricts the output of [SearchPattern ...], [SearchAbout ...], etc. to the names of the symbols matching the @@ -61,7 +61,7 @@ let iter_named_context_name_type f = List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) (* General search over hypothesis of a goal *) -let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = +let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_hyp idh typ = fn (VarRef idh) env typ in let evmap,e = Pfedit.get_goal_context glnum in @@ -69,7 +69,7 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = iter_named_context_name_type iter_hyp pfctxt (* General search over declarations *) -let iter_declarations (fn : global_reference -> env -> constr -> unit) = +let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_obj (sp, kn) lobj = match object_tag lobj with | "VARIABLE" -> @@ -117,8 +117,7 @@ module ConstrPriority = struct (* The priority is memoised here. Because of the very localised use of this module, it is not worth it making a convenient interface. *) - type t = - Globnames.global_reference * Environ.env * Constr.t * priority + type t = GlobRef.t * Environ.env * Constr.t * priority and priority = int module ConstrSet = CSet.Make(Constr) @@ -216,7 +215,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref) let search_about_filter query gr env typ = match query with | GlobSearchSubPattern pat -> - Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat (EConstr.of_constr typ) + Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ) | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s @@ -227,7 +226,7 @@ let search_pattern gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && - pattern_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) && + pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && blacklist_filter ref env typ in let iter ref env typ = @@ -251,8 +250,8 @@ let search_rewrite gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && - (pattern_filter pat1 ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) || - pattern_filter pat2 ref env Evd.empty (EConstr.of_constr typ)) && + (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) || + pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) && blacklist_filter ref env typ in let iter ref env typ = @@ -266,7 +265,7 @@ let search_by_head gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && - head_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) && + head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && blacklist_filter ref env typ in let iter ref env typ = @@ -330,12 +329,12 @@ let interface_search = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (Constr_matching.is_matching env Evd.empty pat (EConstr.of_constr constr)) flag + toggle (Constr_matching.is_matching env (Evd.from_env env) pat (EConstr.of_constr constr)) flag in let match_subtype (pat, flag) = toggle (Constr_matching.is_matching_appsubterm ~closed:false - env Evd.empty pat (EConstr.of_constr constr)) flag + env (Evd.from_env env) pat (EConstr.of_constr constr)) flag in let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag |