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

0 files changed, 0 insertions, 0 deletions