2 files changed, 35 insertions, 60 deletions
diff --git a/test-suite/success/search.v b/test-suite/success/search.v
new file mode 100644
index 0000000000..92de43e052
--- /dev/null
+++ b/test-suite/success/search.v
@@ -0,0 +1,35 @@
+
+(** Test of the different syntaxes of Search *)
+
+Search plus.
+Search plus mult.
+Search "plus_n".
+Search plus "plus_n".
+Search "*".
+Search "*" "+".
+
+Search plus inside Peano.
+Search plus mult inside Peano.
+Search "plus_n" inside Peano.
+Search plus "plus_n" inside Peano.
+Search "*" inside Peano.
+Search "*" "+" inside Peano.
+
+Search plus outside Peano Logic.
+Search plus mult outside Peano Logic.
+Search "plus_n" outside Peano Logic.
+Search plus "plus_n" outside Peano Logic.
+Search "*" outside Peano Logic.
+Search "*" "+" outside Peano Logic.
+
+Search -"*" "+" outside Logic.
+Search -"*"%nat "+"%nat outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+Search Z.mul Z.add "distr".
+Search "+"%Z "*"%Z "distr" -positive -Prop.
+Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
deleted file mode 100644
index 9edfd82556..0000000000
--- a/test-suite/success/searchabout.v
+++ /dev/null
@@ -1,60 +0,0 @@
-
-(** 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 Z.mul Z.add "distr".
-SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
-SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.