From 013e161b7362aefb6a7a9117999e415cce3db9c2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 Jan 2015 11:40:41 +0100
Subject: More in CHANGES about local definitions

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

diff --git a/CHANGES b/CHANGES
index bccb85e8a1..b5b379eca8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -47,7 +47,11 @@ Vernacular commands
   doing "destruct".
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
 - The "Definition" command now allows the "Local" modifier, allowing
-  for non-importable definitions.
+  for non-importable definitions. The same goes for "Axiom" and "Parameter".
+- Section-specific commands such as "Let" (resp. "Variable", "Hypothesis") used
+  out of a section now behave like the corresponding "Local" command, i.e.
+  "Local Definition" (resp. "Local Parameter", "Local Axiom"). (potential source
+  of rare incompatibilities).
 - The "Let" command can now define local (co)fixpoints.
 - Command "Search" has been renamed into "SearchHead". The command
   name "Search" now behaves like former "SearchAbout". The latter name
-- 
cgit v1.2.3