diff options
| author | Jim Fehrle | 2021-01-19 11:55:49 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-01-25 10:26:13 -0800 |
| commit | 3d46bed76e656d6a0e4d87320e4d0fd67d1211c2 (patch) | |
| tree | 7838f1ec474f978474d34d6dd7f06fd9b7c5d58c /vernac/comSearch.ml | |
| parent | 071c50e9c2755e93766e5fb047b0a9065934e8fe (diff) | |
Remove the SearchHead command
Diffstat (limited to 'vernac/comSearch.ml')
| -rw-r--r-- | vernac/comSearch.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index af51f4fafb..1b811f3db7 100644 --- a/vernac/comSearch.ml +++ b/vernac/comSearch.ml @@ -105,12 +105,6 @@ 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 @@ -138,9 +132,6 @@ let interp_search env sigma s r = (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | 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 |> Search.prioritize_search) pr_search); |