From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 vernac/search.ml | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'vernac/search.ml')

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
-- 
cgit v1.2.3