diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-16 12:48:08 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-16 12:48:08 +0100 |
| commit | 37ed28dfe253615729763b5d81a533094fb5425e (patch) | |
| tree | 2940422acc2be9d34585766993d717d52cb46886 /toplevel/search.mli | |
| parent | 8bda62e798c4e89c8c3f9406327899e394f7be0f (diff) | |
Error messages of Searchxxx are coherent with goal selector.
If a goal is given and wrong, exception is raised. If no goal is
given, then goal 1 is tried but no failure if goal 1 does not exist,
just fall back to gloab env.
Diffstat (limited to 'toplevel/search.mli')
| -rw-r--r-- | toplevel/search.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/search.mli b/toplevel/search.mli index f5d1d13ed..2d1d9622d 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -39,10 +39,10 @@ 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 -> constr_pattern -> DirPath.t list * bool -> std_ppcmds -val search_rewrite : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds -val search_pattern : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds -val search_about : int -> (bool * glob_search_about_item) list +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_about : int option -> (bool * glob_search_about_item) list -> DirPath.t list * bool -> std_ppcmds type search_constraint = @@ -68,6 +68,6 @@ val interface_search : (search_constraint * bool) list -> (** {6 Generic search function} *) -val generic_search : int -> display_function -> unit +val generic_search : int option -> display_function -> unit (** This function iterates over all hypothesis of the goal numbered [glnum] (if present) and all known declarations. *) |