1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 416f0a117..6b6892e1d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,9 @@ Vernacular commands
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
 - The "Definition" command now allows the "Local" modifier.
 - 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
+  is deprecated.
 
 Specification Language