Merge PR #10997: Implement the unsupported attribute error using the warning system

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

1 files changed, 9 insertions, 5 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 6af454eee5..b7a3b002bd 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -18,13 +18,17 @@ and vernac_flag_value =
   | VernacFlagLeaf of string
   | VernacFlagList of vernac_flags
 
+let warn_unsupported_attributes =
+  CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError
+    (fun atts ->
+       let keys = List.map fst atts in
+       let keys = List.sort_uniq String.compare keys in
+       let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in
+       Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str"."))
+
 let unsupported_attributes = function
   | [] -> ()
-  | atts ->
-    let keys = List.map fst atts in
-    let keys = List.sort_uniq String.compare keys in
-    let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in
-    user_err Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")
+  | atts -> warn_unsupported_attributes atts
 
 type 'a key_parser = 'a option -> vernac_flag_value -> 'a