Imported Upstream version 8.5~beta1+dfsg

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v
new file mode 100644
index 00000000..2ee8a0d1
--- /dev/null
+++ b/test-suite/output/SearchHead.v
@@ -0,0 +1,19 @@
+(* Some tests of the Search command *)
+
+SearchHead le.				(* app nodes *)
+SearchHead bool. 				(* no apps *)
+SearchHead (@eq nat).			(* complex pattern *)
+
+Definition newdef := fun x:nat => x = x.
+
+Goal forall n:nat, newdef n -> False.
+  intros n h.
+  SearchHead newdef.             (* search hypothesis *)
+Abort.
+
+
+Goal forall n (P:nat -> Prop), P n -> False.
+  intros n P h.
+  SearchHead P.                  (* search hypothesis also for patterns *)
+Abort.
+