aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/searchabout.v
Commit message (Collapse)AuthorAge
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
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