From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/success/intros.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'test-suite/success/intros.v')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 3599da4d..9443d01e 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -3,5 +3,33 @@
 
 Goal forall A, A -> True.
 intros _ _.
+Abort.
 
+(* This did not work until March 2013, because of underlying "red" *)
+Goal (fun x => True -> True) 0.
+intro H.
+Abort.
 
+(* This should still work, with "intro" calling "hnf" *)
+Goal (fun f => True -> f 0 = f 0) (fun x => x).
+intro H.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
+
+(* Somewhat related: This did not work until March 2013 *)
+Goal (fun f => f 0 = f 0) (fun x => x).
+hnf.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
+
+(* Fixing behavior of "*" and "**" in branches, so that they do not
+   introduce more than what the branch expects them to introduce at most *)
+Goal forall n p, n + p = 0.
+intros [|*]; intro p.
+Abort.
+
+(* Check non-interference of "_" with name generation *)
+Goal True -> True -> True.
+intros _ ?.
+exact H.
+Qed.
-- 
cgit v1.2.3