diff options
| author | Hugo Herbelin | 2018-12-08 14:45:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-12 13:30:29 +0100 |
| commit | 412a96a5c3560fee1adad87a3ba1aa1d324ab039 (patch) | |
| tree | 2c76fc72b0fe976514bb2c01737a1fca1af4d6a0 /interp/syntax_def.ml | |
| parent | 84a950c8e1fa06d0dd764e9a426edbd987a7989e (diff) | |
Fixes #9166 (no warning on pattern variables named like a deprecated alias).
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b73d238c22..49273c4146 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -105,3 +105,10 @@ let search_syntactic_definition ?loc kn = let def = out_pat pat in verbose_compat ?loc kn def v; def + +let search_filtered_syntactic_definition ?loc filter kn = + let pat,v = KNmap.find kn !syntax_table in + let def = out_pat pat in + let res = filter def in + (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + res |
