From 70819fdda615b9bb1e897bc82c0ce39b28a2dece Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 15 Dec 2014 13:51:30 +0100
Subject: Tests for Searchxxx commands added and modified.

---
 test-suite/output/SearchPattern.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'test-suite/output/SearchPattern.v')

diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v
index 802d8c9760..bde195a511 100644
--- a/test-suite/output/SearchPattern.v
+++ b/test-suite/output/SearchPattern.v
@@ -17,3 +17,20 @@ 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.
\ No newline at end of file
-- 
cgit v1.2.3