Cleaning the use of pstate and evar_map in Search.

7 files changed, 69 insertions, 78 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index fa458e7c6e..bd99cbed1b 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -341,7 +341,10 @@ let import_search_constraint = function
 
 let search flags =
   let pstate = Vernacstate.Declare.get_pstate () in
-  List.map export_coq_object (Search.interface_search ?pstate (
+  let sigma, env = match pstate with
+  | None -> let env = Global.env () in Evd.(from_env env, env)
+  | Some p -> Declare.get_goal_context p 1 in
+  List.map export_coq_object (Search.interface_search env sigma (
     List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
   )
   [@@ocaml.warning "-3"]
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 568efd86c6..1651e1cc71 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -233,7 +233,7 @@ let rec interp_search_about args accu = match args with
 | [] -> accu
 | (flag, arg) :: rem ->
   fun gr kind env typ ->
-    let ans = Search.search_filter arg gr kind env typ in
+    let ans = Search.search_filter arg gr kind env (Evd.from_env env) typ in
     (if flag then ans else not ans) && interp_search_about rem accu gr kind env typ
 
 let interp_search_arg arg =
@@ -288,10 +288,10 @@ let interp_modloc mr =
     CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in
   let mr_out, mr_in = List.partition fst mr in
   let interp_bmod b = function
-  | [] -> fun _ _ _ _ -> true
+  | [] -> fun _ _ _ _ _ -> true
   | rmods -> Search.module_filter (List.map interp_mod rmods, b) in
   let is_in = interp_bmod false mr_in and is_out = interp_bmod true mr_out in
-  fun gr kind env typ -> is_in gr kind env typ && is_out gr kind env typ
+  fun gr kind env typ -> is_in gr kind env (Evd.from_env env) typ && is_out gr kind env (Evd.from_env env) typ
 
 (* The unified, extended vernacular "Search" command *)
 
@@ -316,5 +316,6 @@ VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
     let display gr kind env typ =
       if post_filter gr kind env typ then ssrdisplaysearch gr env typ
     in
-    Search.generic_search None display }
+    let env = Global.env () in
+    Search.generic_search env display }
 END
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index a527b5e9f8..43f4ed13d9 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -285,3 +285,5 @@ h: P n
 h': ~ P n
 h: P n
 h: P n
+a: A
+b: A
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 82096f29bf..08245a4a91 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -35,3 +35,12 @@ Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
 
 Abort.
 
+Module M.
+Section S.
+Variable A:Type.
+Variable a:A.
+Theorem Thm (b:A) : True.
+Search A. (* Test search in hypotheses *)
+Abort.
+End S.
+End M.
diff --git a/vernac/search.ml b/vernac/search.ml
index 181c75702d..f6b5bbd8e9 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -22,7 +22,7 @@ open Vernacexpr
 module NamedDecl = Context.Named.Declaration
 
 type filter_function =
-  GlobRef.t -> Decls.logical_kind option -> env -> constr -> bool
+  GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool
 type display_function =
   GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit
 
@@ -64,22 +64,6 @@ let iter_constructors indsp u fn env nconstr =
     fn (GlobRef.ConstructRef (indsp, i)) None env typ
   done
 
-let iter_named_context_name_type f =
-  List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
-
-let get_current_or_goal_context ?pstate glnum =
-  match pstate with
-  | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_goal_context p glnum
-
-(* General search over hypothesis of a goal *)
-let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) =
-  let env = Global.env () in
-  let iter_hyp idh typ = fn (GlobRef.VarRef idh) None env typ in
-  let evmap,e = get_current_or_goal_context ?pstate glnum in
-  let pfctxt = named_context e in
-  iter_named_context_name_type iter_hyp pfctxt
-
 (* FIXME: this is a Libobject hack that should be replaced with a proper
    registration mechanism. *)
 module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end)
@@ -89,8 +73,7 @@ let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
 | exception Not_found -> ()
 
 (* General search over declarations *)
-let iter_declarations (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) =
-  let env = Global.env () in
+let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) =
   List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) None env (NamedDecl.get_type d))
     (Environ.named_context env);
   let iter_obj (sp, kn) lobj = match lobj with
@@ -125,12 +108,6 @@ let iter_declarations (fn : GlobRef.t -> Decls.logical_kind option -> env -> con
   try Declaremods.iter_all_segments iter_obj
   with Not_found -> ()
 
-let generic_search ?pstate glnumopt fn =
-  (match glnumopt with
-  | None -> ()
-  | Some glnum -> iter_hypothesis ?pstate glnum fn);
-  iter_declarations fn
-
 (** This module defines a preference on constrs in the form of a
     [compare] function (preferred constr must be big for this
     functions, so preferences such as small constr must use a reversed
@@ -221,12 +198,12 @@ let full_name_of_reference ref =
   DirPath.to_string dir ^ "." ^ Id.to_string id
 
 (** Whether a reference is blacklisted *)
-let blacklist_filter ref kind env typ =
+let blacklist_filter ref kind env sigma typ =
   let name = full_name_of_reference ref in
   let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
   CString.Set.for_all is_not_bl (SearchBlacklist.v ())
 
-let module_filter (mods, outside) ref kind env typ =
+let module_filter (mods, outside) ref kind env sigma typ =
   let sp = Nametab.path_of_global ref in
   let sl = dirpath sp in
   let is_outside md = not (is_dirpath_prefix_of md sl) in
@@ -236,7 +213,7 @@ let module_filter (mods, outside) ref kind env typ =
 
 let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)
 
-let search_filter query gr kind env typ = match query with
+let search_filter query gr kind env sigma typ = match query with
 | GlobSearchSubPattern (where,head,pat) ->
   let open Context.Rel.Declaration in
   let collect_hyps ctx =
@@ -254,7 +231,7 @@ let search_filter query gr kind env typ = match query with
       let f =
         if head then Constr_matching.is_matching_head
         else Constr_matching.is_matching_appsubterm ~closed:false in
-      f env (Evd.from_env env) pat (EConstr.of_constr typ)) typl
+      f env sigma pat (EConstr.of_constr typ)) typl
 | GlobSearchString s ->
   String.string_contains ~where:(name_of_reference gr) ~what:s
 | GlobSearchKind k -> (match kind with None -> false | Some k' -> k = k')
@@ -262,16 +239,16 @@ let search_filter query gr kind env typ = match query with
 
 (** SearchPattern *)
 
-let search_pattern ?pstate gopt pat mods pr_search =
+let search_pattern env sigma pat mods pr_search =
   let filter ref kind env typ =
-    module_filter mods ref kind env typ &&
-    pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref kind env typ
+    module_filter mods ref kind env sigma typ &&
+    pattern_filter pat ref env sigma (EConstr.of_constr typ) &&
+    blacklist_filter ref kind env sigma typ
   in
   let iter ref kind env typ =
     if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 (** SearchRewrite *)
 
@@ -283,49 +260,49 @@ let rewrite_pat1 pat =
 let rewrite_pat2 pat =
   PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |])
 
-let search_rewrite ?pstate gopt pat mods pr_search =
+let search_rewrite env sigma pat mods pr_search =
   let pat1 = rewrite_pat1 pat in
   let pat2 = rewrite_pat2 pat in
   let filter ref kind env typ =
-    module_filter mods ref kind env 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 kind env typ
+    module_filter mods ref kind env sigma typ &&
+    (pattern_filter pat1 ref env sigma (EConstr.of_constr typ) ||
+       pattern_filter pat2 ref env sigma (EConstr.of_constr typ)) &&
+    blacklist_filter ref kind env sigma typ
   in
   let iter ref kind env typ =
     if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 (** Search *)
 
-let search_by_head ?pstate gopt pat mods pr_search =
+let search_by_head env sigma pat mods pr_search =
   let filter ref kind env typ =
-    module_filter mods ref kind env typ &&
-    head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref kind env typ
+    module_filter mods ref kind env sigma typ &&
+    head_filter pat ref env sigma (EConstr.of_constr typ) &&
+    blacklist_filter ref kind env sigma typ
   in
   let iter ref kind env typ =
     if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 (** Search *)
 
-let search ?pstate gopt items mods pr_search =
+let search env sigma items mods pr_search =
   let filter ref kind env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
-    module_filter mods ref kind env typ &&
+    module_filter mods ref kind env sigma typ &&
       let rec aux = function
-        | GlobSearchLiteral i -> search_filter i ref kind env typ
+        | GlobSearchLiteral i -> search_filter i ref kind env sigma typ
         | GlobSearchDisjConj l -> List.exists (List.for_all aux') l
       and aux' (b,s) = eqb b (aux s) in
-      List.for_all aux' items && blacklist_filter ref kind env typ
+      List.for_all aux' items && blacklist_filter ref kind env sigma typ
   in
   let iter ref kind env typ =
     if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 type search_constraint =
   | Name_Pattern of Str.regexp
@@ -340,7 +317,7 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-let interface_search ?pstate =
+let interface_search env sigma =
   let rec extract_flags name tpe subtpe mods blacklist = function
   | [] -> (name, tpe, subtpe, mods, blacklist)
   | (Name_Pattern regexp, b) :: l ->
@@ -354,7 +331,7 @@ let interface_search ?pstate =
   | (Include_Blacklist, b) :: l ->
     extract_flags name tpe subtpe mods b l
   in
-  fun ?glnum flags ->
+  fun flags ->
   let (name, tpe, subtpe, mods, blacklist) =
     extract_flags [] [] [] [] false flags
   in
@@ -366,12 +343,12 @@ let interface_search ?pstate =
       toggle (Str.string_match regexp id 0) flag
     in
     let match_type (pat, flag) =
-      toggle (Constr_matching.is_matching env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
+      toggle (Constr_matching.is_matching env sigma pat (EConstr.of_constr constr)) flag
     in
     let match_subtype (pat, flag) =
       toggle
         (Constr_matching.is_matching_appsubterm ~closed:false
-           env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
+           env sigma pat (EConstr.of_constr constr)) flag
     in
     let match_module (mdl, flag) =
       toggle (Libnames.is_dirpath_prefix_of mdl path) flag
@@ -380,7 +357,7 @@ let interface_search ?pstate =
     List.for_all match_type tpe &&
     List.for_all match_subtype subtpe &&
     List.for_all match_module mods &&
-    (blacklist || blacklist_filter ref kind env constr)
+    (blacklist || blacklist_filter ref kind env sigma constr)
   in
   let ans = ref [] in
   let print_function ref env constr =
@@ -409,5 +386,5 @@ let interface_search ?pstate =
   let iter ref kind env typ =
     if filter_function ref env typ then print_function ref env typ
   in
-  let () = generic_search ?pstate glnum iter in
+  let () = generic_search env iter in
   !ans
diff --git a/vernac/search.mli b/vernac/search.mli
index 3dc437d85a..09847f4e03 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -27,7 +27,7 @@ type glob_search_request =
   | GlobSearchDisjConj of (bool * glob_search_request) list list
 
 type filter_function =
-  GlobRef.t -> Decls.logical_kind option -> env -> constr -> bool
+  GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool
 type display_function =
   GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit
 
@@ -47,13 +47,13 @@ val search_filter : glob_search_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search         : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_request) list
+val search         : env -> Evd.evar_map -> (bool * glob_search_request) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
@@ -74,12 +74,11 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-val interface_search : ?pstate:Declare.Proof.t -> ?glnum:int -> (search_constraint * bool) list ->
-  constr coq_object list
+val interface_search : env -> Evd.evar_map -> (search_constraint * bool) list -> constr coq_object list
 
 (** {6 Generic search function} *)
 
-val generic_search : ?pstate:Declare.Proof.t -> int option -> display_function -> unit
+val generic_search : env -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c7e8d9a3b9..ea79cf7465 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1843,15 +1843,15 @@ let () =
 let vernac_search ~pstate ~atts s gopt r =
   let gopt = query_command_selector gopt in
   let r = interp_search_restriction r in
-  let env,gopt =
+  let sigma, env =
     match gopt with | None ->
       (* 1st goal by default if it exists, otherwise no goal at all *)
-      (try snd (get_goal_or_global_context ~pstate 1) , Some 1
-       with _ -> Global.env (),None)
+      (try get_goal_or_global_context ~pstate 1
+       with _ -> let env = Global.env () in (Evd.from_env env, env))
     (* if goal selector is given and wrong, then let exceptions be raised. *)
-    | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g
+    | Some g -> get_goal_or_global_context ~pstate g
   in
-  let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in
+  let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in
   let warnlist = ref [] in
   let pr_search ref kind env c =
     let pr = pr_global ref in
@@ -1873,13 +1873,13 @@ let vernac_search ~pstate ~atts s gopt r =
   in
   (match s with
   | SearchPattern c ->
-      (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+      (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchRewrite c ->
-      (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+      (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchHead c ->
-      (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+      (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
   | Search sl ->
-      (Search.search ?pstate gopt (List.map (interp_search_request env Evd.(from_env env)) sl) r |>
+      (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |>
        Search.prioritize_search) pr_search);
   if !warnlist <> [] then
   Feedback.msg_notice (str "(" ++