Implement the unsupported attribute error using the warning system

This means we can disable it to ignore unsupported attributes. For
instance this would be useful if we change some behaviour of `Cmd` and add an
attribute `att` to restore the old behaviour, then `#[att] Cmd` is
backwards compatible if the warning is disabled.

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