diff options
| author | herbelin | 2013-07-10 09:24:37 +0000 |
|---|---|---|
| committer | herbelin | 2013-07-10 09:24:37 +0000 |
| commit | 0f281377613d77752289f5d9ce100a25d724df61 (patch) | |
| tree | d1ecf2ca195d84b8f4ca856863eef8c4a3b7d1b7 /test-suite | |
| parent | 84ee4d12817c45d4c299cb0359e066b275360982 (diff) | |
Continuing r16621 on injection intro-patterns:
- order of hypothesis was (historically) from right to left in injection but
already from left to right in decomp_eq, so no need ro fix it there
- made test Injection.v consistent with implementation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16622 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Injection.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index f1ee8a05f7..9d5047fdc3 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. @@ -69,7 +69,7 @@ Abort. (* Test the injection intropattern *) Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b. -intros * (H1,H2). +intros * [= H1 H2]. exact H1. Qed. |