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

1 files changed, 3 insertions, 0 deletions

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
 =========================