diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 10fcf37f21..a7bd150532 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -565,6 +565,9 @@ 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() |