From 33bf4f2c5c60114eb6db4a8e082ff8882923f6c8 Mon Sep 17 00:00:00 2001 From: Vincent Laporte 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 --- CHANGES | 1 + vernac/vernacentries.ml | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/CHANGES b/CHANGES index eaceea6da..9dbc73adb 100644 --- a/CHANGES +++ b/CHANGES @@ -73,6 +73,7 @@ Vernacular Commands was removed. Use Local as a prefix instead. - For the Extraction Language command, "OCaml" is spelled correctly. The older "Ocaml" is still accepted, but deprecated. +- Using “Require” inside a section is deprecated. Universes 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