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, 60 insertions, 0 deletions

diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
new file mode 100644
index 000000000..d9ade3144
--- /dev/null
+++ b/test-suite/success/searchabout.v
@@ -0,0 +1,60 @@
+
+(** Test of the different syntaxes of SearchAbout, in particular
+    with and without the [ ... ] delimiters *)
+
+SearchAbout plus.
+SearchAbout plus mult.
+SearchAbout "plus_n".
+SearchAbout plus "plus_n".
+SearchAbout "*".
+SearchAbout "*" "+".
+
+SearchAbout plus inside Peano.
+SearchAbout plus mult inside Peano.
+SearchAbout "plus_n" inside Peano.
+SearchAbout plus "plus_n" inside Peano.
+SearchAbout "*" inside Peano.
+SearchAbout "*" "+" inside Peano.
+
+SearchAbout plus outside Peano Logic.
+SearchAbout plus mult outside Peano Logic.
+SearchAbout "plus_n" outside Peano Logic.
+SearchAbout plus "plus_n" outside Peano Logic.
+SearchAbout "*" outside Peano Logic.
+SearchAbout "*" "+" outside Peano Logic.
+
+SearchAbout -"*" "+" outside Logic.
+SearchAbout -"*"%nat "+"%nat outside Logic.
+
+SearchAbout [plus].
+SearchAbout [plus mult].
+SearchAbout ["plus_n"].
+SearchAbout [plus "plus_n"].
+SearchAbout ["*"].
+SearchAbout ["*" "+"].
+
+SearchAbout [plus] inside Peano.
+SearchAbout [plus mult] inside Peano.
+SearchAbout ["plus_n"] inside Peano.
+SearchAbout [plus "plus_n"] inside Peano.
+SearchAbout ["*"] inside Peano.
+SearchAbout ["*" "+"] inside Peano.
+
+SearchAbout [plus] outside Peano Logic.
+SearchAbout [plus mult] outside Peano Logic.
+SearchAbout ["plus_n"] outside Peano Logic.
+SearchAbout [plus "plus_n"] outside Peano Logic.
+SearchAbout ["*"] outside Peano Logic.
+SearchAbout ["*" "+"] outside Peano Logic.
+
+SearchAbout [-"*" "+"] outside Logic.
+SearchAbout [-"*"%nat "+"%nat] outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
+SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.