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

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

3 files changed, 17 insertions, 5 deletions

diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst
new file mode 100644
index 0000000000..43a748b365
--- /dev/null
+++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst
@@ -0,0 +1,3 @@
+- The unsupported attribute error is now an error-by-default warning,
+  meaning it can be disabled (`#10997
+  <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ae9d284661..dd65d4aeb3 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1556,6 +1556,11 @@ the following attributes names are recognized:
           now foo.
         Abort.
 
+.. warn:: Unsupported attribute
+
+   This warning is an error by default. It is caused by using a
+   command with some attribute it does not understand.
+
 .. [1]
    This is similar to the expression “*entry* :math:`\{` sep *entry*
    :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry*
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