diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:23:58 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:23:58 +0000 |
| commit | cb7cf50289fbf1c5fe60fd915f63128c88dc6d68 (patch) | |
| tree | 4d60e3ef2cf99c0cdc14e190db378e285494a57f /parsing/search.mli | |
| parent | 557df731a4ad524ebabf78359f950ae063ecef51 (diff) | |
I changed the interface to make sure SearchAbout is defined according to
the same design pattern as the other search commands.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3588 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/search.mli')
| -rw-r--r-- | parsing/search.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/search.mli b/parsing/search.mli index 073a20f87..f7e384e96 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -38,3 +38,5 @@ val raw_pattern_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit +val raw_search_about : (global_reference -> env -> constr -> bool) -> + (global_reference -> env -> constr -> unit) -> global_reference -> unit |