diff options
author | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-27 11:42:55 +0000 |
---|---|---|
committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-27 11:42:55 +0000 |
commit | d58e5b7c7c5a1bca3aa97eb4f8612dc3b85114cd (patch) | |
tree | 1b03d50be9314782e0537ec3e78cbdb3b6d1605a /contrib/interface | |
parent | c947f210f108428c5e63c4a1840cd6ef0c196e16 (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
Diffstat (limited to 'contrib/interface')
-rw-r--r-- | contrib/interface/centaur.ml4 | 6 |
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() |