Renaming search_about_item into search_item.

4 files changed, 9 insertions, 9 deletions

diff --git a/vernac/search.ml b/vernac/search.ml
index 8b54b696f2..92f6d140d5 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -29,7 +29,7 @@ query, separated by a newline. This type of output is useful for
 editors (like emacs), to generate a list of completion candidates
 without having to parse through the types of all symbols. *)
 
-type glob_search_about_item =
+type glob_search_item =
   | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
diff --git a/vernac/search.mli b/vernac/search.mli
index d3b8444b5f..5eeb77a6d0 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -15,7 +15,7 @@ open Pattern
 
 (** {6 Search facilities. } *)
 
-type glob_search_about_item =
+type glob_search_item =
   | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
@@ -30,7 +30,7 @@ val blacklist_filter : filter_function
 val module_filter : DirPath.t list * bool -> filter_function
 (** Check whether a reference pertains or not to a set of modules *)
 
-val search_filter : glob_search_about_item -> filter_function
+val search_filter : glob_search_item -> filter_function
 
 (** {6 Specialized search functions}
 
@@ -44,7 +44,7 @@ val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern ->
                   -> display_function -> unit
 val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search         : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_about_item) list
+val search         : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_item) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 09201d727d..62d97fb845 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1774,7 +1774,7 @@ let interp_search_restriction = function
 
 open Search
 
-let interp_search_about_item env sigma =
+let interp_search_item env sigma =
   function
   | SearchSubPattern pat ->
       let _,pat = Constrintern.intern_constr_pattern env sigma pat in
@@ -1788,7 +1788,7 @@ let interp_search_about_item env sigma =
             ~head:false (fun _ -> true) s sc in
         GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
-        user_err ~hdr:"interp_search_about_item"
+        user_err ~hdr:"interp_search_item"
           (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
 
 (* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the
@@ -1844,7 +1844,7 @@ let vernac_search ~pstate ~atts s gopt r =
   | SearchHead c ->
       (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | Search sl ->
-      (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
+      (Search.search ?pstate gopt (List.map (on_snd (interp_search_item env Evd.(from_env env))) sl) r |>
        Search.prioritize_search) pr_search);
   Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)")
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index b622fd9801..c3ae1993cd 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -61,7 +61,7 @@ type printable =
   | PrintStrategy of qualid or_by_notation option
   | PrintRegistered
 
-type search_about_item =
+type search_item =
   | SearchSubPattern of constr_pattern_expr
   | SearchString of string * scope_name option
 
@@ -69,7 +69,7 @@ type searchable =
   | SearchPattern of constr_pattern_expr
   | SearchRewrite of constr_pattern_expr
   | SearchHead of constr_pattern_expr
-  | Search of (bool * search_about_item) list
+  | Search of (bool * search_item) list
 
 type locatable =
   | LocateAny of qualid or_by_notation