From 33bf4f2c5c60114eb6db4a8e082ff8882923f6c8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 6 Mar 2018 20:29:06 +0000
Subject: [vernac] Warn when using “Require” in a section
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'vernac/vernacentries.ml')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0ff6d9c17..5779c07ab 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -805,7 +805,14 @@ 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.")
+
 let vernac_require from import qidl =
+  if Lib.sections_are_opened () then warn_require_in_section ();
   let qidl = List.map qualid_of_reference qidl in
   let root = match from with
   | None -> None
-- 
cgit v1.2.3