diff options
| author | Théo Zimmermann | 2020-05-12 11:30:25 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:39:09 +0200 |
| commit | eae7b25e06b75f1c890215d4e6176292f10f854a (patch) | |
| tree | 3071f201d0cb97f1264f975375ce79ca49d85a41 /vernac | |
| parent | 7026c498264e32f1ffbeb7767872d00babdbd341 (diff) | |
Deprecate SearchHead.
The main use case of SearchHead is now handled by headconcl:
The secondary use case was redundant with SearchPattern.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comSearch.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index a860bc8bf6..9de8d6fbc3 100644 --- a/vernac/comSearch.ml +++ b/vernac/comSearch.ml @@ -95,6 +95,12 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } +let deprecated_searchhead = + CWarnings.create + ~name:"deprecated-searchhead" + ~category:"deprecated" + (fun () -> Pp.str("SearchHead is deprecated. Use the headconcl: clause of Search instead.")) + let interp_search env sigma s r = let r = interp_search_restriction r in let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in @@ -123,6 +129,7 @@ let interp_search env sigma s r = | SearchRewrite c -> (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> + deprecated_searchhead (); (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | Search sl -> (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |> |