[vernac] Warn when using “Require” in a section

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index eaceea6dad..9dbc73adb7 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