Stop repairing bad relevances in the kernel

It has been default-error for a while, nobody should be relying on it.
SkySkimmer · Jun 14, 2024 · 1833c80 · 1833c80
1 parent ef99688
commit 1833c80
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).