Fix #[warnings] attribute in synterp phase

Fix coq#17982

test-suite/bugs/bug_17982.v

@@ -0,0 +1,8 @@
+
+Set Warnings "+notation-overridden".
+
+Fail Infix "+" := Nat.mul : nat_scope.
+
+#[warnings="-notation-overridden"] Infix "+" := Nat.mul : nat_scope.
+(* Warning: This command does not support this attribute: warnings.
+[unsupported-attributes,parsing,default] *)

vernac/synterp.ml

@@ -47,6 +47,32 @@ let warn_legacy_export_set =
   CWarnings.create ~name:"legacy-export-set" ~category:Deprecation.Version.v8_18
     Pp.(fun () -> strbrk "Syntax \"Export Set\" is deprecated, use the attribute syntax \"#[export] Set\" instead.")
 
+let deprecated_nonuniform =
+  CWarnings.create ~name:"deprecated-nonuniform-attribute"
+    ~category:Deprecation.Version.v8_18
+    Pp.(fun () -> strbrk "Attribute '#[nonuniform]' is deprecated, \
+                          use '#[warning=\"-uniform-inheritance\"]' instead.")
+
+let warnings_att =
+  Attributes.attribute_of_list [
+    "warnings", Attributes.payload_parser ~cat:(^) ~name:"warnings";
+    "warning", Attributes.payload_parser ~cat:(^) ~name:"warning";
+  ]
+
+let with_generic_atts ~check atts f =
+  let atts, warnings = Attributes.parse_with_extra warnings_att atts in
+  let atts, nonuniform = Attributes.parse_with_extra ComCoercion.nonuniform atts in
+  let warnings =
+    let () = if nonuniform <> None && check then deprecated_nonuniform () in
+    if nonuniform <> Some true then warnings else
+      let ui = "-uniform-inheritance" in
+      Some (match warnings with Some w -> w ^ "," ^ ui | None -> ui) in
+  match warnings with
+  | None -> f ~atts
+  | Some warnings ->
+    if check then CWarnings.check_unknown_warnings warnings;
+    CWarnings.with_warn warnings (fun () -> f ~atts) ()
+
 type module_entry = Modintern.module_struct_expr * Names.ModPath.t * Modintern.module_kind * Entries.inline
 
 type control_entry =
@@ -497,7 +523,10 @@ and synterp_load verbosely fname =
   EVernacLoad(verbosely, entries)
 
 and synterp_control CAst.{ loc; v = cmd } =
-  let fn expr = synterp ?loc ~atts:cmd.attrs cmd.expr in
+  let fn expr =
+    with_generic_atts ~check:true cmd.attrs (fun ~atts ->
+        synterp ?loc ~atts cmd.expr)
+  in
   let control, expr = synterp_control_flag ~loc cmd.control fn cmd.expr in
   CAst.make ?loc { expr; control; attrs = cmd.attrs }
 

vernac/synterp.mli

@@ -15,13 +15,16 @@ vernacexpr into a [vernac_control_entry]. *)
 open Names
 open Libnames
 
-val module_locality : bool Attributes.Notations.t
+val module_locality : bool Attributes.attribute
 
 val with_locality : atts:Attributes.vernac_flags -> (local:bool option -> 'a) -> 'a
 
 val with_module_locality :
   atts:Attributes.vernac_flags -> (module_local:bool -> 'a) -> 'a
 
+val with_generic_atts :
+  check:bool -> Attributes.vernac_flags -> (atts:Attributes.vernac_flags -> 'a) -> 'a
+
 type module_entry = Modintern.module_struct_expr * Names.ModPath.t * Modintern.module_kind * Entries.inline
 
 type control_entry =

vernac/vernacentries.ml

@@ -908,7 +908,7 @@ let preprocess_inductive_decl ~atts kind indl =
   in
   (* We only allow the #[projections(primitive)] attribute
      for records. *)
-  let prim_proj_attr : bool Attributes.Notations.t =
+  let prim_proj_attr : bool Attributes.attribute =
     if List.for_all is_record indl then primitive_proj
     else Notations.return false
   in

vernac/vernacinterp.ml

@@ -104,32 +104,6 @@ let interp_control_entry ~loc (f : control_entry) ~st
   | ControlRedirect s ->
     Topfmt.with_output_to_file s (fun () -> fn ~st) ()
 
-let deprecated_nonuniform =
-  CWarnings.create ~name:"deprecated-nonuniform-attribute"
-    ~category:Deprecation.Version.v8_18
-    Pp.(fun () -> strbrk "Attribute '#[nonuniform]' is deprecated, \
-                          use '#[warning=\"-uniform-inheritance\"]' instead.")
-
-let warnings_att =
-  Attributes.attribute_of_list [
-    "warnings", Attributes.payload_parser ~cat:(^) ~name:"warnings";
-    "warning", Attributes.payload_parser ~cat:(^) ~name:"warning";
-  ]
-
-let with_generic_atts atts f =
-  let atts, warnings = Attributes.parse_with_extra warnings_att atts in
-  let atts, nonuniform = Attributes.parse_with_extra ComCoercion.nonuniform atts in
-  let warnings =
-    let () = if nonuniform <> None then deprecated_nonuniform () in
-    if nonuniform <> Some true then warnings else
-      let ui = "-uniform-inheritance" in
-      Some (match warnings with Some w -> w ^ "," ^ ui | None -> ui) in
-  match warnings with
-  | None -> f ~atts
-  | Some warnings ->
-    CWarnings.check_unknown_warnings warnings;
-    CWarnings.with_warn warnings (fun () -> f ~atts) ()
-
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
@@ -183,7 +157,7 @@ and interp_control ~st ({ CAst.v = cmd; loc }) =
     cmd.control
     (fun ~st ->
        let before_univs = Global.universes () in
-       let pstack, pm = with_generic_atts cmd.attrs (fun ~atts ->
+       let pstack, pm = with_generic_atts ~check:false cmd.attrs (fun ~atts ->
            interp_expr ?loc ~atts ~st cmd.expr)
        in
        let after_univs = Global.universes () in