From 8df7d4bb994b4d29698be8ca7fadba3caf6add75 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 19 Nov 2010 10:20:07 +0000
Subject: SearchAbout: who has never been annoyed by the [ ] syntax ?

 Well, hopefully, that belongs to the past: you should now be able
 to do the very same queries as before, without typing the [ ].
 For instance: SearchAbout plus mult.

 This removal of [ ] is optional, the old syntax is still legal:
  - for compatibility reasons
  - for square bracket lovers
  - for those that have "inside" or "outside" as legal identifier
    in their development and want to search about them.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13654 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 2d3ac54268..f749f1f1b7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,9 @@ Changes from V8.3 to V8.4
   the universe graph is printed in the DOT language, and can be
   processed by Graphviz tools.
 
+Vernacular commands
+
+- In SearchAbout, the [ ] delimiters are now optional.
 
 Changes from V8.2 to V8.3
 =========================
-- 
cgit v1.2.3