From 262a4e28744a81a433d387486d96a583f893c7e8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Mar 2018 14:03:07 +0200
Subject: CHANGES: mentioning new command "Declare Scope".

---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGES b/CHANGES
index 5d1c9a9c2d..738c0934d1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,11 @@ Notations
 - New support for autonomous grammars of terms, called "custom
   entries" (see chapter "Syntax extensions" of the reference manual).
 
+- New command "Declare Scope" to explicitly declare a scope name
+  before any use of it. Implicit declaration of a scope at the time of
+  "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is
+  deprecated.
+
 Tactics
 
 - Added toplevel goal selector ! which expects a single focused goal.
-- 
cgit v1.2.3