Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as pattern variables

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