From 6ab4479dfa0f9b8fd4df4342fdfdab6c25b62fb7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 12:10:53 +0100
Subject: Improving syntax of pat/constr introduction pattern so that
 pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.

Open to other suggestions of syntax though.
---
 test-suite/success/intros.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 35ba94fb67..741f372ff2 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -69,3 +69,12 @@ intros H (H1,?)/H.
 change (1=1) in H0.
 exact H1.
 Qed.
+
+(* Checking iterated pat/c1.../cn introduction patterns and side conditions *)
+
+Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D.
+intros * H H0 H1.
+intros H2/H/H0.
+- exact H2.
+- exact H1.
+Qed.
-- 
cgit v1.2.3