aboutsummaryrefslogtreecommitdiff
path: root/interp/syntax_def.ml
diff options
context:
space:
mode:
authorHugo Herbelin2018-12-08 14:45:28 +0100
committerHugo Herbelin2018-12-12 13:30:29 +0100
commit412a96a5c3560fee1adad87a3ba1aa1d324ab039 (patch)
tree2c76fc72b0fe976514bb2c01737a1fca1af4d6a0 /interp/syntax_def.ml
parent84a950c8e1fa06d0dd764e9a426edbd987a7989e (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.ml7
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