diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 14:17:09 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 20:00:03 +0100 |
| commit | 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae (patch) | |
| tree | 7c2a4361b949c5f496bdee7d56ce9f8aaa878277 /toplevel | |
| parent | 9130ea9cbc657cd7adf02830e40a89f6de3953f3 (diff) | |
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
There are currently two other clashs : Lexer and Errors, but for
the moment these ones haven't impacted my experiments with extraction
and compiler-libs, while this Matching issue had. And anyway the new
name is more descriptive, in the spirit of the recent TacticMatching.
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 91762c000..78fa3a325 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -114,7 +114,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 Matching.is_matching pat typ then true + if ConstrMatching.is_matching pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ @@ -122,7 +122,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 Matching.is_matching_head pat typ then true + if ConstrMatching.is_matching_head pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> head_filter pat ref env typ @@ -151,7 +151,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 -> - Matching.is_matching_appsubterm ~closed:false pat typ + ConstrMatching.is_matching_appsubterm ~closed:false pat typ | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s @@ -277,10 +277,11 @@ let interface_search flags = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (Matching.is_matching pat constr) flag + toggle (ConstrMatching.is_matching pat constr) flag in let match_subtype (pat, flag) = - toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag + toggle + (ConstrMatching.is_matching_appsubterm ~closed:false pat constr) flag in let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag |