diff options
Diffstat (limited to 'toplevel/search.mli')
| -rw-r--r-- | toplevel/search.mli | 21 |
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} *) |