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/search.ml | |
| parent | 071c50e9c2755e93766e5fb047b0a9065934e8fe (diff) | |
Remove the SearchHead command
Diffstat (limited to 'vernac/search.ml')
| -rw-r--r-- | vernac/search.ml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/vernac/search.ml b/vernac/search.ml index 501e5b1a91..98e231de19 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -185,14 +185,6 @@ let rec pattern_filter pat ref env sigma typ = | LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ | _ -> false -let rec head_filter pat ref env sigma typ = - let typ = Termops.strip_outer_cast sigma typ in - if Constr_matching.is_matching_head env sigma pat typ then true - else match EConstr.kind sigma typ with - | Prod (_, _, typ) - | LetIn (_, _, _, typ) -> head_filter pat ref env sigma typ - | _ -> false - let full_name_of_reference ref = let (dir,id) = repr_path (Nametab.path_of_global ref) in DirPath.to_string dir ^ "." ^ Id.to_string id @@ -274,19 +266,6 @@ let search_rewrite env sigma pat mods pr_search = (** Search *) -let search_by_head env sigma pat mods pr_search = - let filter ref kind env typ = - module_filter mods ref kind env sigma typ && - head_filter pat ref env sigma (EConstr.of_constr typ) && - blacklist_filter ref kind env sigma typ - in - let iter ref kind env typ = - if filter ref kind env typ then pr_search ref kind env typ - in - generic_search env iter - -(** Search *) - let search env sigma items mods pr_search = let filter ref kind env typ = let eqb b1 b2 = if b1 then b2 else not b2 in |