Merge PR #10180: `deprecated` attribute support for notations and syntactic definitions

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin

23 files changed, 276 insertions, 198 deletions

diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index ff9b32fe78..0338cd42c7 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -73,8 +73,6 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
 COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
 G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
-BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
-BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
                          for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
@@ -401,34 +399,6 @@ dev/tools/update-compat.py --assert-unchanged %s || exit $?
 ''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip()
     update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args)
 
-def update_bug_4789(new_versions, **args):
-    # we always update this compat notation to oldest
-    # currently-supported compat version, which should never be the
-    # current version
-    with open(BUG_4798_PATH, 'r') as f: contents = f.read()
-    new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "%s").
-Check match 2 with 0 => 0 | S n => n end. (* fails *)
-""" % new_versions[0]
-    update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
-
-def update_bug_9166(new_versions, **args):
-    # we always update this compat notation to oldest
-    # currently-supported compat version, which should never be the
-    # current version
-    with open(BUG_9166_PATH, 'r') as f: contents = f.read()
-    new_contents = BUG_HEADER + r"""Set Warnings "+deprecated".
-
-Notation bar := option (compat "%s").
-
-Definition foo (x: nat) : nat :=
-  match x with
-  | 0 => 0
-  | S bar => bar
-  end.
-""" % new_versions[0]
-    update_if_changed(contents, new_contents, BUG_9166_PATH, **args)
-
 def update_compat_notations_in(old_versions, new_versions, contents):
     for v in old_versions:
         if v not in new_versions:
@@ -508,7 +478,5 @@ if __name__ == '__main__':
     update_test_suite(new_versions, **args)
     update_test_suite_run(**args)
     update_doc_index(new_versions, **args)
-    update_bug_4789(new_versions, **args)
-    update_bug_9166(new_versions, **args)
     update_compat_notations(known_versions, new_versions, **args)
     display_git_grep(known_versions, new_versions)
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst
new file mode 100644
index 0000000000..01f2e893ed
--- /dev/null
+++ b/doc/changelog/03-notations/10180-deprecate-notations.rst
@@ -0,0 +1,6 @@
+- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated`
+  attribute. The former `compat` annotation for notations is
+  deprecated, and its semantics changed. It is now made equivalent to using
+  a `deprecated` attribute, and is no longer connected with the `-compat`
+  command-line flag.
+  (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès).
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ebaa6fde66..38f6714f46 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1508,7 +1508,10 @@ the following attributes names are recognized:
     Takes as value the optional attributes ``since`` and ``note``;
     both have a string value.
 
-    This attribute can trigger the following warnings:
+    This attribute is supported by the following commands: :cmd:`Ltac`,
+    :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`.
+
+    It can trigger the following warnings:
 
     .. warn:: Tactic @qualid is deprecated since @string. @string.
        :undocumented:
@@ -1516,6 +1519,11 @@ the following attributes names are recognized:
     .. warn:: Tactic Notation @qualid is deprecated since @string. @string.
        :undocumented:
 
+    .. warn:: Notation @string__1 is deprecated since @string__2. @string__3.
+
+       :n:`@string__1` is the actual notation, :n:`@string__2` is the version number,
+       :n:`@string__3` is the note.
+
 .. example::
 
    .. coqtop:: all reset warn
diff --git a/interp/deprecation.ml b/interp/deprecation.ml
new file mode 100644
index 0000000000..b6f0dceb89
--- /dev/null
+++ b/interp/deprecation.ml
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type t = { since : string option ; note : string option }
+
+let make ?since ?note () = { since ; note }
+
+let create_warning ~object_name ~warning_name name_printer =
+  let open Pp in
+  CWarnings.create ~name:warning_name ~category:"deprecated"
+    (fun (qid,depr) -> str object_name ++ spc () ++ name_printer qid ++
+      strbrk " is deprecated" ++
+      pr_opt (fun since -> str "since " ++ str since) depr.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.note)
diff --git a/interp/deprecation.mli b/interp/deprecation.mli
new file mode 100644
index 0000000000..aab87c11a2
--- /dev/null
+++ b/interp/deprecation.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type t = { since : string option ; note : string option }
+
+val make : ?since:string -> ?note:string -> unit -> t
+
+val create_warning : object_name:string -> warning_name:string ->
+  ('b -> Pp.t) -> ?loc:Loc.t -> 'b * t -> unit
diff --git a/interp/interp.mllib b/interp/interp.mllib
index b65a171ef9..52978a2ab6 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+Deprecation
 NumTok
 Constrexpr
 Tactypes
diff --git a/interp/notation.ml b/interp/notation.ml
index a7bac96d31..cc06d5abfc 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -72,6 +72,7 @@ type notation_location = (DirPath.t * DirPath.t) * string
 type notation_data = {
   not_interp : interpretation;
   not_location : notation_location;
+  not_deprecation : Deprecation.t option;
 }
 
 type scope = {
@@ -1095,7 +1096,7 @@ let warn_notation_overridden =
                     str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
                     ++ strbrk "was already used" ++ which_scope ++ str ".")
 
-let declare_notation_interpretation ntn scopt pat df ~onlyprint =
+let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   if not onlyprint then begin
@@ -1109,6 +1110,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
     let notdata = {
       not_interp = pat;
       not_location = df;
+      not_deprecation = deprecation;
     } in
     let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in
     scope_map := String.Map.add scope sc !scope_map
@@ -1125,10 +1127,10 @@ let declare_uninterpretation rule (metas,c as pat) =
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
   | Scope scope :: scopes ->
-      (try let (pat,df) = find scope in pat,(df,Some scope)
+      (try let n = find scope in (n,Some scope)
        with Not_found -> find_interpretation ntn find scopes)
   | SingleNotation ntn'::scopes when notation_eq ntn' ntn ->
-      (try let (pat,df) = find default_scope in pat,(df,None)
+      (try let n = find default_scope in (n,None)
        with Not_found ->
          (* e.g. because single notation only for constr, not cases_pattern *)
          find_interpretation ntn find scopes)
@@ -1136,8 +1138,7 @@ let rec find_interpretation ntn find = function
       find_interpretation ntn find scopes
 
 let find_notation ntn sc =
-  let n = NotationMap.find ntn (find_scope sc).notations in
-  (n.not_interp, n.not_location)
+  NotationMap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
   | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
@@ -1147,7 +1148,9 @@ let notation_of_prim_token = function
 let find_prim_token check_allowed ?loc p sc =
   (* Try for a user-defined numerical notation *)
   try
-    let (_,c),df = find_notation (notation_of_prim_token p) sc in
+    let n = find_notation (notation_of_prim_token p) sc in
+    let (_,c) = n.not_interp in
+    let df = n.not_location in
     let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in
     check_allowed pat;
     pat, df
@@ -1167,7 +1170,9 @@ let find_prim_token check_allowed ?loc p sc =
 let interp_prim_token_gen ?loc g p local_scopes =
   let scopes = make_current_scopes local_scopes in
   let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
-  try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
+  try
+    let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
+    pat, (loc,sc)
   with Not_found ->
     user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
@@ -1192,11 +1197,18 @@ let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function
 let interp_prim_token_cases_pattern_expr ?loc looked_for p =
   interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p
 
+let warn_deprecated_notation =
+  Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-notation"
+    pr_notation
+
 let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
-  try find_interpretation ntn (find_notation ntn) scopes
+  try
+    let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
+    Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation;
+    n.not_interp, (n.not_location, sc)
   with Not_found ->
-    user_err ?loc 
+    user_err ?loc
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
 let uninterp_notations c =
diff --git a/interp/notation.mli b/interp/notation.mli
index a67948a778..b32561d908 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -217,7 +217,8 @@ type interp_rule =
   | SynDefRule of KerName.t
 
 val declare_notation_interpretation : notation -> scope_name option ->
-      interpretation -> notation_location -> onlyprint:bool -> unit
+  interpretation -> notation_location -> onlyprint:bool ->
+  Deprecation.t option -> unit
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a7e1de736c..8df04187f1 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -19,20 +19,24 @@ open Notation_term
 
 (* Syntactic definitions. *)
 
-type version = Flags.compat_version option
+type syndef =
+  { syndef_pattern : interpretation;
+    syndef_onlyparsing : bool;
+    syndef_deprecation : Deprecation.t option;
+  }
 
 let syntax_table =
-  Summary.ref (KNmap.empty : (interpretation*version) KNmap.t)
-    ~name:"SYNTAXCONSTANT"
+  Summary.ref (KNmap.empty : syndef KNmap.t)
+    ~name:"SYNDEFS"
 
-let add_syntax_constant kn c onlyparse =
-  syntax_table := KNmap.add kn (c,onlyparse) !syntax_table
+let add_syntax_constant kn syndef =
+  syntax_table := KNmap.add kn syndef !syntax_table
 
-let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(_local,syndef)) =
   if Nametab.exists_cci sp then
     user_err ~hdr:"cache_syntax_constant"
       (Id.print (basename sp) ++ str " already exists");
-  add_syntax_constant kn pat onlyparse;
+  add_syntax_constant kn syndef;
   Nametab.push_syndef (Nametab.Until i) sp kn
 
 let is_alias_of_already_visible_name sp = function
@@ -42,30 +46,29 @@ let is_alias_of_already_visible_name sp = function
   | _ ->
       false
 
-let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
+let open_syntax_constant i ((sp,kn),(_local,syndef)) =
+  let pat = syndef.syndef_pattern in
   if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
     Nametab.push_syndef (Nametab.Exactly i) sp kn;
-    match onlyparse with
-    | None ->
+    if not syndef.syndef_onlyparsing then
       (* Redeclare it to be used as (short) name in case an other (distfix)
          notation was declared in between *)
       Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
-    | _ -> ()
   end
 
 let cache_syntax_constant d =
   load_syntax_constant 1 d;
   open_syntax_constant 1 d
 
-let subst_syntax_constant (subst,(local,pat,onlyparse)) =
-  (local,Notation_ops.subst_interpretation subst pat,onlyparse)
+let subst_syntax_constant (subst,(local,syndef)) =
+  let syndef_pattern = Notation_ops.subst_interpretation subst syndef.syndef_pattern in
+  (local, { syndef with syndef_pattern })
 
-let classify_syntax_constant (local,_,_ as o) =
+let classify_syntax_constant (local,_ as o) =
   if local then Dispose else Substitute o
 
-let in_syntax_constant
- : bool * interpretation * Flags.compat_version option -> obj =
-  declare_object {(default_object "SYNTAXCONSTANT") with
+let in_syntax_constant : (bool * syndef) -> obj =
+  declare_object {(default_object "SYNDEF") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
     open_function = open_syntax_constant;
@@ -79,36 +82,31 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
 let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
 
-let declare_syntactic_definition local id onlyparse pat =
-  let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
-
-let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
-
-let pr_compat_warning (kn, def, v) =
-  let pp_def = match def with
-    | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r
-    | _ -> strbrk " is a compatibility notation"
+let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
+  let syndef =
+    { syndef_pattern = in_pat pat;
+      syndef_onlyparsing = onlyparsing;
+      syndef_deprecation = deprecation;
+    }
   in
-  pr_syndef kn ++ pp_def
+  let _ = add_leaf id (in_syntax_constant (local,syndef)) in ()
 
-let warn_compatibility_notation =
-  CWarnings.(create ~name:"compatibility-notation"
-                    ~category:"deprecated" ~default:Enabled pr_compat_warning)
+let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
 
-let verbose_compat ?loc kn def = function
-  | Some v when Flags.version_strictly_greater v ->
-     warn_compatibility_notation ?loc (kn, def, v)
-  | _ -> ()
+let warn_deprecated_syntactic_definition =
+  Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition"
+    pr_syndef
 
 let search_syntactic_definition ?loc kn =
-  let pat,v = KNmap.find kn !syntax_table in
-  let def = out_pat pat in
-  verbose_compat ?loc kn def v;
+  let syndef = KNmap.find kn !syntax_table in
+  let def = out_pat syndef.syndef_pattern in
+  Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
   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 syndef = KNmap.find kn !syntax_table in
+  let def = out_pat syndef.syndef_pattern in
   let res = filter def in
-  (match res with Some _ -> verbose_compat ?loc kn def v | None -> ());
+  if Option.has_some res then
+    Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
   res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 77873f8f67..e6e3b9cffa 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -15,8 +15,8 @@ open Notation_term
 
 type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 
-val declare_syntactic_definition : bool -> Id.t ->
-  Flags.compat_version option -> syndef_interpretation -> unit
+val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
+  onlyparsing:bool -> syndef_interpretation -> unit
 
 val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
 
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 309db539d0..2cc6f9a279 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,11 +12,10 @@
 
 open Vernacexpr
 open Tacexpr
-open Attributes
 
 (** {5 Tactic Definitions} *)
 
-val register_ltac : locality_flag -> ?deprecation:deprecation ->
+val register_ltac : locality_flag -> ?deprecation:Deprecation.t ->
   Tacexpr.tacdef_body list -> unit
 (** Adds new Ltac definitions to the environment. *)
 
@@ -36,7 +35,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol
     leaves. *)
 
 val add_tactic_notation :
-  locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+  locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument
   grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
 (** [add_tactic_notation local level prods expr] adds a tactic notation in the
     environment at level [level] with locality [local] made of the grammar
@@ -49,7 +48,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
     to finding an argument by name (as in {!Genarg}) if there is none
     matching. *)
 
-val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:Deprecation.t ->
   argument grammar_tactic_prod_item_expr list list -> unit
 (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
     ML-side macro. *)
@@ -80,7 +79,7 @@ type _ ty_sig =
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
 val tactic_extend : string -> string -> level:Int.t ->
-  ?deprecation:deprecation -> ty_ml list -> unit
+  ?deprecation:Deprecation.t -> ty_ml list -> unit
 
 (** {5 ARGUMENT EXTEND} *)
 
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5f22b2c72..3347f594d2 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -55,7 +55,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Attributes.deprecation option;
+    alias_deprecation: Deprecation.t option;
   }
 
 let alias_map = Summary.ref ~name:"tactic-alias"
@@ -121,7 +121,7 @@ type ltac_entry = {
   tac_for_ml : bool;
   tac_body : glob_tactic_expr;
   tac_redef : ModPath.t list;
-  tac_deprecation : Attributes.deprecation option
+  tac_deprecation : Deprecation.t option
 }
 
 let mactab =
@@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) =
 let classify_md (local, _, _, _, _ as o) = Substitute o
 
 let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
-           Attributes.deprecation option -> obj =
+           Deprecation.t option -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 5b98daf383..2fc45760d1 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,7 +12,6 @@ open Names
 open Libnames
 open Tacexpr
 open Geninterp
-open Attributes
 
 (** This module centralizes the various ways of registering tactics. *)
 
@@ -33,7 +32,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: deprecation option;
+    alias_deprecation: Deprecation.t option;
   }
 (** Contents of a tactic notation *)
 
@@ -48,7 +47,7 @@ val check_alias : alias -> bool
 
 (** {5 Coq tactic definitions} *)
 
-val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
+val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Id.t ->
   glob_tactic_expr -> unit
 (** Register a new Ltac with the given name and body.
 
@@ -57,7 +56,7 @@ val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
     definition. It also puts the Ltac name in the nametab, so that it can be
     used unqualified. *)
 
-val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t ->
+val redefine_ltac : bool -> ?deprecation:Deprecation.t -> KerName.t ->
   glob_tactic_expr -> unit
 (** Replace a Ltac with the given name and body. If the boolean flag is set
     to true, then this is a local redefinition. *)
@@ -68,7 +67,7 @@ val interp_ltac : KerName.t -> glob_tactic_expr
 val is_ltac_for_ml_tactic : KerName.t -> bool
 (** Whether the tactic is defined from ML-side *)
 
-val tac_deprecation : KerName.t -> deprecation option
+val tac_deprecation : KerName.t -> Deprecation.t option
 (** The tactic deprecation notice, if any *)
 
 type ltac_entry = {
@@ -78,7 +77,7 @@ type ltac_entry = {
   (** The current body of the tactic *)
   tac_redef : ModPath.t list;
   (** List of modules redefining the tactic in reverse chronological order *)
-  tac_deprecation : deprecation option;
+  tac_deprecation : Deprecation.t option;
   (** Deprecation notice to be printed when the tactic is used *)
 }
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index c1f7fab123..7434f81946 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -119,18 +119,13 @@ let intern_constr_reference strict ist qid =
 (* Internalize an isolated reference in position of tactic *)
 
 let warn_deprecated_tactic =
-  CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
-    (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
-      strbrk " is deprecated" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
+  Deprecation.create_warning ~object_name:"Tactic" ~warning_name:"deprecated-tactic"
+    pr_qualid
 
 let warn_deprecated_alias =
-  CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
-    (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
-      strbrk " is deprecated since" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
+  Deprecation.create_warning ~object_name:"Tactic Notation"
+    ~warning_name:"deprecated-tactic-notation"
+    Pptactic.pr_alias_key
 
 let intern_isolated_global_tactic_reference qid =
   let loc = qid.CAst.loc in
diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v
deleted file mode 100644
index f238086633..0000000000
--- a/test-suite/bugs/closed/bug_4798.v
+++ /dev/null
@@ -1,5 +0,0 @@
-(* DO NOT MODIFY THIS FILE DIRECTLY *)
-(* It is autogenerated by dev/tools/update-compat.py. *)
-Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.8").
-Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v
index 21cd770cbb..cd594c660f 100644
--- a/test-suite/bugs/closed/bug_9166.v
+++ b/test-suite/bugs/closed/bug_9166.v
@@ -1,8 +1,7 @@
-(* DO NOT MODIFY THIS FILE DIRECTLY *)
-(* It is autogenerated by dev/tools/update-compat.py. *)
 Set Warnings "+deprecated".
 
-Notation bar := option (compat "8.8").
+#[deprecated(since = "X", note = "Y")]
+Notation bar := option.
 
 Definition foo (x: nat) : nat :=
   match x with
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
new file mode 100644
index 0000000000..d313ba0aa4
--- /dev/null
+++ b/test-suite/success/NotationDeprecation.v
@@ -0,0 +1,62 @@
+Module Syndefs.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation foo := Prop.
+
+Notation bar := Prop (compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation zar := Prop (compat "8.8").
+
+Check foo.
+Check bar.
+
+Set Warnings "+deprecated".
+
+Fail Check foo.
+Fail Check bar.
+
+End Syndefs.
+
+Module Notations.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation "!!" := Prop.
+
+Notation "##" := Prop (compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation "**" := Prop (compat "8.8").
+
+Check !!.
+Check ##.
+
+Set Warnings "+deprecated".
+
+Fail Check !!.
+Fail Check ##.
+
+End Notations.
+
+Module Infix.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Infix "!!" := plus (at level 1).
+
+Infix "##" := plus (at level 1, compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Infix "**" := plus (at level 1, compat "8.8").
+
+Check (_ !! _).
+Check (_ ## _).
+
+Set Warnings "+deprecated".
+
+Fail Check (_ !! _).
+Fail Check (_ ## _).
+
+End Infix.
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 4576ff4cbe..bb4ed10bc9 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -149,6 +149,7 @@ apply AC_IF.
 Qed.
 
 
-Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8").
+#[deprecated(since = "8.8", note = "Use classical_proof_irrelevance instead.")]
+Notation classical_proof_irrelevence := classical_proof_irrelevance.
 
 End Berardis_paradox.
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 1ad5862d5d..ab14974598 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -73,11 +73,6 @@ module Notations = struct
 end
 open Notations
 
-type deprecation = { since : string option ; note : string option }
-
-let mk_deprecation ?(since=None) ?(note=None) () =
-  { since ; note }
-
 let assert_empty k v =
   if v <> VernacFlagEmpty
   then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
@@ -213,19 +208,16 @@ let polymorphic =
   universe_transform ~warn_unqualified:true >>
   qualify_attribute ukey polymorphic_base
 
-let deprecation_parser : deprecation key_parser = fun orig args ->
+let deprecation_parser : Deprecation.t key_parser = fun orig args ->
   assert_once ~name:"deprecation" orig;
   match args with
   | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
   | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
-    let since = Some since and note = Some note in
-    mk_deprecation ~since ~note ()
+    Deprecation.make ~since ~note ()
   | VernacFlagList [ "since", VernacFlagLeaf since ] ->
-    let since = Some since in
-    mk_deprecation ~since ()
+    Deprecation.make ~since ()
   | VernacFlagList [ "note", VernacFlagLeaf note ] ->
-    let note = Some note in
-    mk_deprecation ~note ()
+    Deprecation.make ~note ()
   |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
 
 let deprecation = attribute_of_list ["deprecated",deprecation_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 44688ddafc..53caf49efd 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -43,15 +43,11 @@ end
 
 (** Definitions for some standard attributes. *)
 
-type deprecation = { since : string option ; note : string option }
-
-val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
-
 val polymorphic : bool attribute
 val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
-val deprecation : deprecation option attribute
+val deprecation : Deprecation.t option attribute
 val canonical : bool attribute
 
 val program_mode_option_name : string list
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 50914959dc..b96f500beb 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -732,13 +732,8 @@ type syntax_extension = {
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
   synext_extra : (string * string) list;
-  synext_compat : Flags.compat_version option;
 }
 
-let is_active_compat = function
-| None -> true
-| Some v -> 0 <= Flags.version_compare v !Flags.compat_version
-
 type syntax_extension_obj = locality_flag * syntax_extension
 
 let check_and_extend_constr_grammar ntn rule =
@@ -759,7 +754,7 @@ let cache_one_syntax_extension se =
     let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
     if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
   with Not_found ->
-    if is_active_compat se.synext_compat then begin
+    begin
       (* Reserve the notation level *)
       Notgram_ops.declare_notation_level ntn prec ~onlyprint;
       (* Declare the parsing rule *)
@@ -934,10 +929,6 @@ let is_only_printing mods =
   let test = function SetOnlyPrinting -> true | _ -> false in
   List.exists test mods
 
-let get_compat_version mods =
-  let test = function SetCompatVersion v -> Some v | _ -> None in
-  try Some (List.find_map test mods) with Not_found -> None
-
 (* Compute precedences from modifiers (or find default ones) *)
 
 let set_entry_type from etyps (x,typ) =
@@ -1177,7 +1168,7 @@ module SynData = struct
     (* Fields coming from the vernac-level modifiers *)
     only_parsing  : bool;
     only_printing : bool;
-    compat        : Flags.compat_version option;
+    deprecation   : Deprecation.t option;
     format        : lstring option;
     extra         : (string * string) list;
 
@@ -1222,12 +1213,32 @@ let check_locality_compatibility local custom i_typs =
                     strbrk " which is local."))
       (List.uniquize allcustoms)
 
-let compute_syntax_data local df modifiers =
+let warn_deprecated_compat =
+  CWarnings.create ~name:"deprecated-compat" ~category:"deprecated"
+    (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++
+                   str"Please use the \"deprecated\" attributed instead."))
+
+(* Returns the new deprecation and the onlyparsing status. This should be
+removed together with the compat syntax modifier. *)
+let merge_compat_deprecation compat deprecation =
+  match compat, deprecation with
+  | Some Flags.Current, _ -> deprecation, true
+  | Some _, Some _ ->
+    CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute."
+                        ++ spc () ++ str"Please use only the latter.")
+  | Some v, None ->
+    warn_deprecated_compat ();
+    Some (Deprecation.make ~since:(Flags.pr_version v) ()), true
+  | None, Some _ -> deprecation, true
+  | None, None -> deprecation, false
+
+let compute_syntax_data ~local deprecation df modifiers =
   let open SynData in
   let open NotationMods in
   let mods = interp_modifiers modifiers in
   let onlyprint = mods.only_printing in
   let onlyparse = mods.only_parsing in
+  let deprecation, _ = merge_compat_deprecation mods.compat deprecation in
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
   let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
@@ -1265,7 +1276,7 @@ let compute_syntax_data local df modifiers =
 
     only_parsing  = mods.only_parsing;
     only_printing = mods.only_printing;
-    compat        = mods.compat;
+    deprecation;
     format        = mods.format;
     extra         = mods.extra;
 
@@ -1281,9 +1292,9 @@ let compute_syntax_data local df modifiers =
     not_data    = sy_fulldata;
   }
 
-let compute_pure_syntax_data local df mods =
+let compute_pure_syntax_data ~local df mods =
   let open SynData in
-  let sd = compute_syntax_data local df mods in
+  let sd = compute_syntax_data ~local None df mods in
   let msgs =
     if sd.only_parsing then
       (Feedback.msg_warning ?loc:None,
@@ -1301,7 +1312,7 @@ type notation_obj = {
   notobj_coercion : entry_coercion_kind option;
   notobj_onlyparse : bool;
   notobj_onlyprint : bool;
-  notobj_compat : Flags.compat_version option;
+  notobj_deprecation : Deprecation.t option;
   notobj_notation : notation * notation_location;
 }
 
@@ -1323,11 +1334,11 @@ let open_notation i (_, nobj) =
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
   let onlyprint = nobj.notobj_onlyprint  in
+  let deprecation = nobj.notobj_deprecation in
   let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
-  let active = is_active_compat nobj.notobj_compat in
-  if Int.equal i 1 && fresh && active then begin
+  if Int.equal i 1 && fresh then begin
     (* Declare the interpretation *)
-    let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
+    let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
     (* Declare the uninterpretation *)
     if not nobj.notobj_onlyparse then
       Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
@@ -1388,7 +1399,6 @@ let recover_notation_syntax ntn =
       synext_notgram = pa_rule;
       synext_unparsing = pp_rule;
       synext_extra = pp_extra_rules;
-      synext_compat = None;
     }
   with Not_found ->
     raise NoSyntaxRule
@@ -1437,7 +1447,6 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
     synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
     synext_unparsing = pp_rule;
     synext_extra  = sd.extra;
-    synext_compat = sd.compat;
   }
 
 (**********************************************************************)
@@ -1447,9 +1456,9 @@ let to_map l =
   let fold accu (x, v) = Id.Map.add x v accu in
   List.fold_left fold Id.Map.empty l
 
-let add_notation_in_scope local df env c mods scope =
+let add_notation_in_scope ~local deprecation df env c mods scope =
   let open SynData in
-  let sd = compute_syntax_data local df mods in
+  let sd = compute_syntax_data ~local deprecation df mods in
   (* Prepare the interpretation *)
   (* Prepare the parsing and printing rules *)
   let sy_rules = make_syntax_rules sd in
@@ -1470,7 +1479,7 @@ let add_notation_in_scope local df env c mods scope =
     notobj_onlyparse = onlyparse;
     notobj_coercion = coe;
     notobj_onlyprint = sd.only_printing;
-    notobj_compat = sd.compat;
+    notobj_deprecation = sd.deprecation;
     notobj_notation = sd.info;
   } in
   (* Ready to change the global state *)
@@ -1479,7 +1488,7 @@ let add_notation_in_scope local df env c mods scope =
   Lib.add_anonymous_leaf (inNotation notation);
   sd.info
 
-let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
+let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation =
   let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
@@ -1510,7 +1519,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
     notobj_onlyparse = onlyparse;
     notobj_coercion = coe;
     notobj_onlyprint = onlyprint;
-    notobj_compat = compat;
+    notobj_deprecation = deprecation;
     notobj_notation = df';
   } in
   Lib.add_anonymous_leaf (inNotation notation);
@@ -1518,41 +1527,40 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
 
 (* Notations without interpretation (Reserved Notation) *)
 
-let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
-  let psd = compute_pure_syntax_data local df mods in
-  let sy_rules = make_syntax_rules {psd with compat = None} in
+let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
+  let psd = compute_pure_syntax_data ~local df mods in
+  let sy_rules = make_syntax_rules {psd with deprecation = None} in
   Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
 (* Notations with only interpretation *)
 
 let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
-  let df' = add_notation_interpretation_core false df env c sc false false None in
+  let df' = add_notation_interpretation_core ~local:false df env c sc false false None in
   Dumpglob.dump_notation (loc,df') sc true
 
 let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
   (try ignore
-    (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
+    (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ());
   with NoSyntaxRule ->
     user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
 
 (* Main entry point *)
 
-let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
+let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc =
   let df' =
    if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
     let onlyparse = is_only_parsing modifiers in
     let onlyprint = is_only_printing modifiers in
-    let compat = get_compat_version modifiers in
-    try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat
+    try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
-      add_notation_in_scope local df env c modifiers sc
+      add_notation_in_scope ~local deprecation df env c modifiers sc
    else
     (* Declare both syntax and interpretation *)
-    add_notation_in_scope local df env c modifiers sc
+    add_notation_in_scope ~local deprecation df env c modifiers sc
   in
   Dumpglob.dump_notation (loc,df') sc true
 
@@ -1566,7 +1574,7 @@ let add_notation_extra_printing_rule df k v =
 
 let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None)
 
-let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
+let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc =
   check_infix_modifiers modifiers;
   (* check the precedence *)
   let vars = names_of_constr_expr pr in
@@ -1575,7 +1583,7 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
   let metas = [inject_var x; inject_var y] in
   let c = mkAppC (pr,metas) in
   let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
-  add_notation local env c (df,modifiers) sc
+  add_notation ~local deprecation env c (df,modifiers) sc
 
 (**********************************************************************)
 (* Scopes, delimiters and classes bound to scopes                     *)
@@ -1651,7 +1659,7 @@ let try_interp_name_alias = function
   | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
   | _ -> raise Not_found
 
-let add_syntactic_definition env ident (vars,c) local onlyparse =
+let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
   let vars,reversibility,pat =
     try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
     with Not_found ->
@@ -1665,11 +1673,9 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
       let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, reversibility, pat
   in
-  let onlyparse = match onlyparse with
-    | None when fst (printability None false reversibility pat) -> Some Flags.Current
-    | p -> p
-  in
-  Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+  let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in
+  let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
+  Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
 
 (**********************************************************************)
 (* Declaration of custom entry                                        *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 6435df23c7..6532cee367 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -19,10 +19,10 @@ val add_token_obj : string -> unit
 
 (** Adding a (constr) notation in the environment*)
 
-val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) ->
+val add_infix : local:bool -> Deprecation.t option -> env -> (lstring * syntax_modifier list) ->
   constr_expr -> scope_name option -> unit
 
-val add_notation : locality_flag -> env -> constr_expr ->
+val add_notation : local:bool -> Deprecation.t option -> env -> constr_expr ->
   (lstring * syntax_modifier list) -> scope_name option -> unit
 
 val add_notation_extra_printing_rule : string -> string -> string -> unit
@@ -47,12 +47,12 @@ val set_notation_for_interpretation : env -> Constrintern.internalization_env ->
 (** Add only the parsing/printing rule of a notation *)
 
 val add_syntax_extension :
-  locality_flag -> (lstring * syntax_modifier list) -> unit
+  local:bool -> (lstring * syntax_modifier list) -> unit
 
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
-val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
-  bool -> Flags.compat_version option -> unit
+val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
+  Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit
 
 (** Print the Camlp5 state of a grammar *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d206165e88..112c4b6451 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -81,7 +81,7 @@ module DefAttributes = struct
     locality : bool option;
     polymorphic : bool;
     program : bool;
-    deprecated : deprecation option;
+    deprecated : Deprecation.t option;
   }
 
   let parse f =
@@ -92,6 +92,8 @@ module DefAttributes = struct
     { polymorphic; program; locality; deprecated }
 end
 
+let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
+
 let with_locality ~atts f =
   let local = Attributes.(parse locality atts) in
   f ~local
@@ -102,8 +104,7 @@ let with_section_locality ~atts f =
   f ~section_local
 
 let with_module_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  let module_local = make_module_locality local in
+  let module_local = Attributes.(parse module_locality atts) in
   f ~module_local
 
 let with_def_attributes ~atts f =
@@ -504,7 +505,7 @@ let dump_global r =
 
 let vernac_syntax_extension ~module_local infix l =
   if infix then Metasyntax.check_infix_modifiers (snd l);
-  Metasyntax.add_syntax_extension module_local l
+  Metasyntax.add_syntax_extension ~local:module_local l
 
 let vernac_declare_scope ~module_local sc =
   Metasyntax.declare_scope module_local sc
@@ -523,11 +524,13 @@ let vernac_open_close_scope ~section_local (b,s) =
 let vernac_arguments_scope ~section_local r scl =
   Notation.declare_arguments_scope section_local (smart_global r) scl
 
-let vernac_infix ~module_local =
-  Metasyntax.add_infix module_local (Global.env())
+let vernac_infix ~atts =
+  let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+  Metasyntax.add_infix ~local:module_local deprecation (Global.env())
 
-let vernac_notation ~module_local =
-  Metasyntax.add_notation module_local (Global.env())
+let vernac_notation ~atts =
+  let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+  Metasyntax.add_notation ~local:module_local deprecation (Global.env())
 
 let vernac_custom_entry ~module_local s =
   Metasyntax.declare_custom_entry module_local s
@@ -1265,9 +1268,10 @@ let vernac_hints ~atts dbnames h =
   let local = enforce_module_locality local in
   Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
 
-let vernac_syntactic_definition ~module_local lid x y =
+let vernac_syntactic_definition ~atts lid x compat =
+  let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
   Dumpglob.dump_definition lid false "syndef";
-  Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
+  Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
 
 let cache_bidi_hints (_name, (gr, ohint)) =
   match ohint with
@@ -2379,9 +2383,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacOpenCloseScope (b, s) ->
     VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s))
   | VernacInfix (mv,qid,sc) ->
-    VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc)
+    VtDefault(fun () -> vernac_infix ~atts mv qid sc)
   | VernacNotation (c,infpl,sc) ->
-    VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc)
+    VtDefault(fun () -> vernac_notation ~atts c infpl sc)
   | VernacNotationAddFormat(n,k,v) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
@@ -2559,8 +2563,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
     VtDefault(fun () ->
         vernac_hints ~atts dbnames hints)
   | VernacSyntacticDefinition (id,c,b) ->
-    VtDefault(fun () ->
-        with_module_locality ~atts vernac_syntactic_definition id c b)
+    VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
   | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
     VtDefault(fun () ->
         with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))