From 192ce3da462b3eba13b88e8940ce1751d351e25e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Jun 2013 21:31:34 +0000
Subject: Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as
 an "injection" tactic when applied on an equality statement. Moreover,
 hypotheses are now entered in the left-to-right order.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16550 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Injection.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index c5cd7380a2..9847e09872 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -66,6 +66,13 @@ einjection (H O).
 instantiate (1:=O).
 Abort.
 
+(* Test the injection intropattern *)
+
+Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b.
+intros * (H1,H2).
+exact H1.
+Qed.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
-- 
cgit v1.2.3