diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-26 13:43:02 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-26 13:43:02 +0000 |
| commit | c947f210f108428c5e63c4a1840cd6ef0c196e16 (patch) | |
| tree | 79696a6691de55c245522f940a2568949da3db52 /toplevel | |
| parent | b657956f17442f33ba4fc80fe6720e9a238bcb31 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/search.ml | 13 | ||||
| -rw-r--r-- | toplevel/search.mli | 6 |
2 files changed, 9 insertions, 10 deletions
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 |