1 files changed, 24 insertions, 20 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index fd80cec6..f8f7c996 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -2,33 +2,37 @@
 
 (* Check that Injection tries Intro until *)
 
-Lemma l1 : (x:nat)(S x)=(S (S x))->False.
-Injection 1.
-Apply n_Sn.
+Lemma l1 : forall x : nat, S x = S (S x) -> False.
+ injection 1.
+apply n_Sn.
 Qed.
 
-Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False.
-Injection H.
-Intros.
-Apply (n_Sn x H0).
+Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False.
+ injection H.
+intros.
+apply (n_Sn x H0).
 Qed.
 
 (* Check that no tuple needs to be built *)
-Lemma l3 : (x,y:nat)
-     (existS ? [n:nat]({n=n}+{n=n}) x (left ? ? (refl_equal nat x)))=
-     (existS ? [n:nat]({n=n}+{n=n}) y (left ? ? (refl_equal nat y)))
-  -> x=y.
-Intros x y H.
-Injection H.
-Exact [H]H.
+Lemma l3 :
+ forall x y : nat,
+ existS (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) =
+ existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) -> 
+ x = y.
+intros x y H.
+ injection H.
+exact (fun H => H).
 Qed.
 
 (* Check that a tuple is built (actually the same as the initial one) *)
-Lemma l4 : (p1,p2:{O=O}+{O=O})
-    (existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2)
-  ->(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2).
-Intros.
-Injection H.
-Exact [H]H.
+Lemma l4 :
+ forall p1 p2 : {0 = 0} + {0 = 0},
+ existS (fun n : nat => {n = n} + {n = n}) 0 p1 =
+ existS (fun n : nat => {n = n} + {n = n}) 0 p2 ->
+ existS (fun n : nat => {n = n} + {n = n}) 0 p1 =
+ existS (fun n : nat => {n = n} + {n = n}) 0 p2.
+intros.
+ injection H.
+exact (fun H => H).
 Qed.