Merge PR #11974: Require in Section: warning is now about fragility not deprecation.

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

1 files changed, 3 insertions, 4 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 106fed124e..9a1d935928 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1081,10 +1081,9 @@ let vernac_end_segment ({v=id} as lid) =
 (* Libraries *)
 
 let warn_require_in_section =
-  let name = "require-in-section" in
-  let category = "deprecated" in
-  CWarnings.create ~name ~category
-    (fun () -> strbrk "Use of “Require” inside a section is deprecated.")
+  CWarnings.create ~name:"require-in-section" ~category:"fragile"
+    (fun () -> strbrk "Use of “Require” inside a section is fragile." ++ spc() ++
+               strbrk "It is not recommended to use this functionality in finished proof scripts.")
 
 let vernac_require from import qidl =
   if Global.sections_are_opened () then warn_require_in_section ();