Nouveaux tests

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4049 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index aecb7e1f6..fd80cec6f 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -12,3 +12,23 @@ 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.
+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.
+Qed.
+