diff options
Diffstat (limited to 'vernac/search.mli')
| -rw-r--r-- | vernac/search.mli | 15 |
1 files changed, 7 insertions, 8 deletions
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. *) |