1 files changed, 51 insertions, 1 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index c5cd7380..6a488244 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -39,7 +39,7 @@ Qed.
 (* Test injection as *)
 
 Lemma l5 : forall x y z t : nat, (x,y) = (z,t) -> x=z.
-intros; injection H as Hyt Hxz.
+intros; injection H as Hxz Hyt.
 exact Hxz.
 Qed.
 
@@ -66,6 +66,56 @@ 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.
+
+(* 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.
+
+(* Test injection using K, knowing that an equality is decidable *)
+(* Basic case, using sigT, with "as" clause *)
+
+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 as H.
+exact H.
+Abort.
+
+(* Test injection using K, knowing that an equality is decidable *)
+(* Dependent case not directly exposing sigT *)
+
+Inductive my_sig (A : Type) (P : A -> Type) : Type :=
+    my_exist : forall x : A, P x -> my_sig A P.
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  my_exist _ _ n H1 = my_exist _ _ n H2 -> H1 = H2.
+intros.
+injection H as H.
+exact H.
+Abort.
+
+(* Test injection using K, knowing that an equality is decidable *)
+(* Dependent case not directly exposing sigT deeply nested *)
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  (my_exist _ _ n H1,0) = (my_exist _ _ n H2,0) -> H1 = H2.
+intros * [= H].
+exact H.
+Abort.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.