diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /test-suite/success/Injection.v | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'test-suite/success/Injection.v')
-rw-r--r-- | test-suite/success/Injection.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index f8f7c996..606e884a 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -36,3 +36,29 @@ intros. exact (fun H => H). Qed. +(* Test injection as *) + +Lemma l5 : forall x y z t : nat, (x,y) = (z,t) -> x=z. +intros; injection H as Hyt Hxz. +exact Hxz. +Qed. + +(* Injection does not projects at positions in Prop... allow it? + +Inductive t (A:Prop) : Set := c : A -> t A. +Goal forall p q : True\/True, c _ p = c _ q -> False. +intros. +injection H. +Abort. + +*) + +(* Accept does not project on discriminable positions... allow it? + +Goal 1=2 -> 1=0. +intro H. +injection H. +intro; assumption. +Qed. + + *) |