diff options
| author | herbelin | 2003-11-10 09:28:03 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-10 09:28:03 +0000 |
| commit | c1ff0876818e3c75fe6f075f433369437c20b982 (patch) | |
| tree | f18be83ef64cf728d3a31c309bd7907442cc3adf /contrib/interface | |
| parent | 53e3a6a6d2d9673f8ba83797b0cdf1ec37f0fd7c (diff) | |
Suppression SearchNamed finalement redondant avec SearchAbout
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 3 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 3 |
2 files changed, 1 insertions, 5 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index f4a8580eb2..c86d12ad2a 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -569,9 +569,6 @@ let pcoq_search s l = | SearchHead locqid -> filtered_search (filter_by_module_from_list l) add_search (Nametab.global locqid) - | SearchNamed strings -> - raw_search_named - (filter_by_module_from_list l) add_search strings end; search_output_results() diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 3d57d24857..3f3c3ba615 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1502,8 +1502,7 @@ let xlate_vernac = | SearchHead id -> CT_search(loc_qualid_to_ct_ID id, xlate_search_restr x) | SearchRewrite c -> xlate_error "TODO: SearchRewrite" - | SearchAbout id -> xlate_error "TODO: SearchAbout" - | SearchNamed id -> xlate_error "TODO: SearchNamed") + | SearchAbout id -> xlate_error "TODO: SearchAbout") | (*Record from tactics/Record.v *) VernacRecord |