Fix #5242 - Dubious unsilenceable warning on invalid identifier

We make this warning configurable and disabled by default.

1 files changed, 7 insertions, 1 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 9267a64d6..1eb9a3175 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,9 +34,15 @@ struct
 
   let hash = String.hash
 
+  let warn_invalid_identifier =
+    CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
+                     ~default:CWarnings.Disabled
+                     (fun s -> str s)
+
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x)
+      if fatal then CErrors.error x else
+        if warn then warn_invalid_identifier x
     in
     Option.iter iter (Unicode.ident_refutation x)