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

4 files changed, 24 insertions, 3 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 40922b5c35..7aa85a0810 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1527,8 +1527,8 @@ let drop_notations_pattern looked_for genv =
     try
       match Nametab.locate_extended qid with
       | SynDef sp ->
-	let (vars,a) = Syntax_def.search_syntactic_definition sp in
-	(match a with
+        let filter (vars,a) =
+        try match a with
 	| NRef g ->
           (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	  test_kind top g;
@@ -1549,7 +1549,9 @@ let drop_notations_pattern looked_for genv =
               let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
 	      let (_,argscs) = find_remaining_scopes pats1 pats2 g in
 	      Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
-	| _ -> raise Not_found)
+        | _ -> raise Not_found
+        with Not_found -> None in
+        Syntax_def.search_filtered_syntactic_definition filter sp
       | TrueGlobal g ->
 	  test_kind top g;
           Dumpglob.add_glob ?loc:qid.loc g;
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
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index c5b6655ff8..77873f8f67 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -19,3 +19,6 @@ val declare_syntactic_definition : bool -> Id.t ->
   Flags.compat_version option -> syndef_interpretation -> unit
 
 val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
+
+val search_filtered_syntactic_definition : ?loc:Loc.t ->
+  (syndef_interpretation -> 'a option) -> KerName.t -> 'a option
diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v
new file mode 100644
index 0000000000..8a7e9c37b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9166.v
@@ -0,0 +1,9 @@
+Set Warnings "+deprecated".
+
+Notation bar := option (compat "8.7").
+
+Definition foo (x: nat) : nat :=
+  match x with
+  | 0 => 0
+  | S bar => bar
+  end.