1 files changed, 36 insertions, 0 deletions
diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v
new file mode 100644
index 0000000000..de9f48873a
--- /dev/null
+++ b/test-suite/output/SearchPattern.v
@@ -0,0 +1,36 @@
+(* Some tests of the SearchPattern command *)
+
+(* Simple, random tests *)
+SearchPattern bool.
+SearchPattern nat.
+SearchPattern le.
+
+(* With some hypothesis *)
+SearchPattern (nat -> nat).
+SearchPattern (?n * ?m + ?n = ?n * S ?m).
+
+(* Non-linearity *)
+SearchPattern (_ ?X ?X).
+
+(* Non-linearity with hypothesis *)
+SearchPattern (forall (x:?A) (y:?B), _ ?A ?B).
+
+(* No delta-reduction *)
+SearchPattern (Exc _).
+
+Definition newdef := fun x:nat => x.
+
+Goal forall n:nat, n <> newdef n -> False.
+  intros n h.
+  SearchPattern ( _ <> newdef _).          (* search hypothesis *)
+  SearchPattern ( n <> newdef _).          (* search hypothesis *)
+Abort.
+
+Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
+  intros n P h h'.
+  SearchPattern (P _).      (* search hypothesis also for patterns *)
+  Search (~P n).          (* search hypothesis also for patterns *)
+  Search (P _) -"h'".       (* search hypothesis also for patterns *)
+  Search (P _) -not.       (* search hypothesis also for patterns *)
+
+Abort.