diff options
| -rw-r--r-- | contrib/interface/centaur.ml4 | 3 | ||||
| -rw-r--r-- | parsing/search.mli | 2 |
2 files changed, 5 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() diff --git a/parsing/search.mli b/parsing/search.mli index d477659e34..d53c3fecf3 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -41,3 +41,5 @@ val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_about : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> global_reference -> unit +val raw_search_named : (global_reference -> env -> constr -> bool) -> + (global_reference -> env -> constr -> unit) -> string list -> unit |