Imported Upstream version 8.6upstream/8.6

1 files changed, 12 insertions, 9 deletions

diff --git a/toplevel/search.mli b/toplevel/search.mli
index 78b0c45c..ba3d48ef 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -39,21 +39,24 @@ val search_about_filter : glob_search_about_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_pattern : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_by_head : int option -> constr_pattern -> DirPath.t list * bool
+                  -> display_function -> unit
+val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool
+                  -> display_function -> unit
+val search_pattern : int option -> constr_pattern -> DirPath.t list * bool
+                  -> display_function -> unit
 val search_about   : int option -> (bool * glob_search_about_item) list
-  -> DirPath.t list * bool -> std_ppcmds
+                  -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
   (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
-  | Name_Pattern of string
+  | Name_Pattern of Str.regexp
   (** Whether the object type satisfies a pattern *)
-  | Type_Pattern of string
+  | Type_Pattern of Pattern.constr_pattern
   (** Whether some subtype of object type satisfies a pattern *)
-  | SubType_Pattern of string
+  | SubType_Pattern of Pattern.constr_pattern
   (** Whether the object pertains to a module *)
-  | In_Module of string list
+  | In_Module of Names.DirPath.t
   (** Bypass the Search blacklist *)
   | Include_Blacklist
 
@@ -63,7 +66,7 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-val interface_search : (search_constraint * bool) list ->
+val interface_search : ?glnum:int -> (search_constraint * bool) list ->
   string coq_object list
 
 (** {6 Generic search function} *)