From c947f210f108428c5e63c4a1840cd6ef0c196e16 Mon Sep 17 00:00:00 2001 From: puech Date: Mon, 26 Jan 2009 13:43:02 +0000 Subject: Revert changes in pcoq functions to restore compatibility with contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11859 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/search.ml | 13 ++++++------- toplevel/search.mli | 6 +++--- 2 files changed, 9 insertions(+), 10 deletions(-) (limited to 'toplevel') diff --git a/toplevel/search.ml b/toplevel/search.ml index e50af9733..481d91787 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -165,6 +165,9 @@ let raw_search_rewrite extra_filter display_function pattern = && extra_filter s a c) display_function gref_eq +let raw_search_by_head extra_filter display_function pattern = + Util.todo "raw_search_by_head" + (* * functions to use the new Libtypes facility *) @@ -178,18 +181,14 @@ let raw_search search_function extra_filter display_function pat = display_function gr env typ ) (search_function pat) -let raw_pattern_search = raw_search Libtypes.search_concl -let raw_search_rewrite = raw_search (Libtypes.search_eq_concl c_eq) -let raw_search_by_head = raw_search Libtypes.search_head_concl - let text_pattern_search extra_filter = - raw_pattern_search extra_filter plain_display + raw_search Libtypes.search_concl extra_filter plain_display let text_search_rewrite extra_filter = - raw_search_rewrite extra_filter plain_display + raw_search (Libtypes.search_eq_concl c_eq) extra_filter plain_display let text_search_by_head extra_filter = - raw_search_by_head extra_filter plain_display + raw_search Libtypes.search_head_concl extra_filter plain_display let filter_by_module_from_list = function | [], _ -> (fun _ _ _ -> true) diff --git a/toplevel/search.mli b/toplevel/search.mli index 5b978770b..96163f7da 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -42,11 +42,11 @@ val gen_filtered_search : (global_reference -> env -> constr -> bool) -> val filtered_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> global_reference -> unit val raw_pattern_search : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr -> unit + (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr -> unit + (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_about : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> (bool * glob_search_about_item) list -> unit val raw_search_by_head : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr -> unit + (global_reference -> env -> constr -> unit) -> constr_pattern -> unit -- cgit v1.2.3