aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-27 11:42:55 +0000
committerGravatar puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-27 11:42:55 +0000
commitd58e5b7c7c5a1bca3aa97eb4f8612dc3b85114cd (patch)
tree1b03d50be9314782e0537ec3e78cbdb3b6d1605a
parentc947f210f108428c5e63c4a1840cd6ef0c196e16 (diff)
Forgot a file in r11859. Sorry...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11860 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/interface/centaur.ml46
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 79fa912a6..f8c088779 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -565,13 +565,13 @@ let pcoq_search s l =
raw_search_about (filter_by_module_from_list l) add_search
(List.map (on_snd interp_search_about_item) sl)
| SearchPattern c ->
- let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
raw_pattern_search (filter_by_module_from_list l) add_search pat
| SearchRewrite c ->
- let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
raw_search_rewrite (filter_by_module_from_list l) add_search pat;
| SearchHead c ->
- let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
raw_search_by_head (filter_by_module_from_list l) add_search pat;
end;
search_output_results()