diff options
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 |