From a417d138c0a8abc028486c20d59e4f2e82f456ef Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 12 Dec 2014 15:19:10 +0100
Subject: Searchxxx now search also the hypothesis and support goal selector.

Documentation also updated.
---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index b1946188b4..5c1a27fa6f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -52,6 +52,11 @@ Vernacular commands
 - Command "Search" has been renamed into "SearchHead". The command
   name "Search" now behaves like former "SearchAbout". The latter name
   is deprecated.
+- "Search" "SearchHead" "SearchRewrite" and "SearchPattern" now search
+  for hypothesis (of the current goal) first. They now also support the
+  goal selector prefix to specify another goal to search: e.g.
+  "n:Search id". This is also true for SearchAbout although it is
+  deprecated.
 - The coq/user-contrib directory and the XDG directories are no longer
   recursively added to the load path, so files from installed libraries
   now need to be fully qualified for the "Require" command to find them.
-- 
cgit v1.2.3