"Warnings" and "Debug" options are synterp not interp

SkySkimmer · Jan 9, 2025 · 84f409c · 84f409c
1 parent 7c3baa6
commit 84f409c
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 2 deletions.
diff --git a/dev/ci/user-overlays/19981-SkySkimmer-classify-warn.sh b/dev/ci/user-overlays/19981-SkySkimmer-classify-warn.sh
@@ -0,0 +1 @@
+overlay metacoq https://github.com/SkySkimmer/metacoq classify-warn 19981
diff --git a/doc/changelog/08-vernac-commands-and-options/19981-classify-warn.rst b/doc/changelog/08-vernac-commands-and-options/19981-classify-warn.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  :opt:`Debug` and :opt:`Warnings` are classified as Synterp.
+  This changes the scheduling during :cmd:`Import` such that putting `#[export] Set Warnings` around a specific command may change behaviour.
+  (`#19981 <https://github.com/coq/coq/pull/19981>`_,
+  by Gaëtan Gilbert).
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
@@ -1967,15 +1967,15 @@ let () =
     CWarnings.normalize_flags_string flags
   in
   declare_string_option ~preprocess
-    { optstage = Summary.Stage.Interp;
+    { optstage = Summary.Stage.Synterp;
       optdepr  = None;
       optkey   = ["Warnings"];
       optread  = CWarnings.get_flags;
       optwrite = CWarnings.set_flags }
 
 let () =
   declare_string_option
-    { optstage = Summary.Stage.Interp;
+    { optstage = Summary.Stage.Synterp;
       optdepr  = None;
       optkey   = ["Debug"];
       optread  = CDebug.get_flags;
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		overlay metacoq https://github.com/SkySkimmer/metacoq classify-warn 19981