diff options
| author | Matthieu Sozeau | 2014-08-25 21:46:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-25 21:55:34 +0200 |
| commit | 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e (patch) | |
| tree | f7860f13dc18938953ead65c63923aba117d890b /toplevel | |
| parent | 12c803053572194c85e4c7b7f347175c7c335858 (diff) | |
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/search.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml index e2a4ad25cf..6a7d2c8118 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -98,7 +98,7 @@ let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l) (** FIXME: this is quite dummy, we may find a more efficient algorithm. *) let rec pattern_filter pat ref env typ = let typ = strip_outer_cast typ in - if ConstrMatching.is_matching pat typ then true + if ConstrMatching.is_matching env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ @@ -106,7 +106,7 @@ let rec pattern_filter pat ref env typ = let rec head_filter pat ref env typ = let typ = strip_outer_cast typ in - if ConstrMatching.is_matching_head pat typ then true + if ConstrMatching.is_matching_head env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> head_filter pat ref env typ @@ -135,7 +135,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref) let search_about_filter query gr env typ = match query with | GlobSearchSubPattern pat -> - ConstrMatching.is_matching_appsubterm ~closed:false pat typ + ConstrMatching.is_matching_appsubterm ~closed:false env Evd.empty pat typ | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s @@ -274,11 +274,12 @@ let interface_search flags = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (ConstrMatching.is_matching pat constr) flag + toggle (ConstrMatching.is_matching env Evd.empty pat constr) flag in let match_subtype (pat, flag) = toggle - (ConstrMatching.is_matching_appsubterm ~closed:false pat constr) flag + (ConstrMatching.is_matching_appsubterm ~closed:false + env Evd.empty pat constr) flag in let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag |