Merge PR #7135: Introducing an explicit `Declare Scope` command

1 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 0ccbb10657..81693a8166 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.