Merge PR coq#19164: Stop repairing bad relevances in the kernel

Reviewed-by: ppedrot Ack-by: silene Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Jun 18, 2024 · 5ea287a · 5ea287a
2 parents 763fb02 + 1833c80
commit 5ea287a
Show file tree

Hide file tree

Showing 7 changed files with 122 additions and 196 deletions.
diff --git a/checker/checker.ml b/checker/checker.ml
@@ -386,7 +386,6 @@ let init_with_argv argv =
   let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
   try
     parse_args argv;
-    CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name);
     if CDebug.(get_flag misc) then Printexc.record_backtrace true;
     Flags.if_verbose print_header ();
     if not !boot then init_load_path ();

diff --git a/doc/changelog/01-kernel/19164-good-triumps-when-bad-relevances-are-errors.rst b/doc/changelog/01-kernel/19164-good-triumps-when-bad-relevances-are-errors.rst
@@ -0,0 +1,6 @@
+- **Removed:**
+  the kernel always produces an error when given terms with bad relevances
+  instead of emitting the default-error `bad-relevance` warning
+  (which is now only used by the higher layers)
+  (`#19164 <https://github.com/coq/coq/pull/19164>`_,
+  by Gaëtan Gilbert).