From 84ee4d12817c45d4c299cb0359e066b275360982 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 9 Jul 2013 22:32:52 +0000
Subject: Revising r16550 about providing intro patterns for applying
 injection: - Introduction of a specific notation for injection intropatterns:
 [= pats] - Use of this specific pattern also to apply discriminate on the fly

Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).

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

(limited to 'test-suite')

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 9847e09872..f1ee8a05f7 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -73,6 +73,17 @@ intros * (H1,H2).
 exact H1.
 Qed.
 
+(* Test injection using K, knowing that an equality is decidable *)
+(* Basic case, using sigT *)
+
+Scheme Equality for nat.
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  existT P n H1 = existT P n H2 -> H1 = H2.
+intros.
+injection H.
+intro H0. exact H0.
+Abort.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
-- 
cgit v1.2.3