aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-03-06 20:29:06 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-03-07 17:31:47 +0000
commit33bf4f2c5c60114eb6db4a8e082ff8882923f6c8 (patch)
treea07c626739bf195b5d7a938c5fe4ee5594c2c1a1 /vernac
parent66c523bcac8b64e202baa084bf24f5b57c61fcd6 (diff)
[vernac] Warn when using “Require” in a section
Diffstat (limited to 'vernac')
-rw-r--r--vernac/vernacentries.ml7
1 files changed, 7 insertions, 0 deletions
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