From 083ab9fb9ac3b63d741e342cfb2a847968a6784e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 May 2020 10:54:15 +0200
Subject: Require in Section: warning is now about fragility not deprecation.

---
 vernac/vernacentries.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac')

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 ();
-- 
cgit v1.2.3