Fixed hypotheses of Z_lt_induction (see #957)

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

1 files changed, 6 insertions, 7 deletions

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index e44262a5b..131460a75 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -283,7 +283,7 @@ clear v3 Hv3; intros.
 elim (Z_zerop x); intro.
 apply Euclid_intro with (u := u1) (v := u2) (d := u3).
 assumption.
-apply H2.
+apply H3.
 rewrite a0; auto with zarith.
 set (q := u3 / x) in *.
 assert (Hq : 0 <= u3 - q * x < x).
@@ -297,9 +297,9 @@ apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)).
 tauto.
 replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with
  (u1 * a + u2 * b - q * (v1 * a + v2 * b)).
-rewrite H0; rewrite H1; trivial.
+rewrite H1; rewrite H2; trivial.
 ring.
-intros; apply H2.
+intros; apply H3.
 apply Zis_gcd_for_euclid with q; assumption.
 assumption.
 Qed.
@@ -381,7 +381,7 @@ apply
     (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}));
  try assumption.
 intro x; case x.
-intros _ b; exists (Zabs b).
+intros _ _ b; exists (Zabs b).
   elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)).
     intros H0; split.
     apply Zabs_ind.
@@ -393,7 +393,7 @@ intros _ b; exists (Zabs b).
     rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *.
     split; [ apply Zis_gcd_0 | idtac ]; auto with zarith.
   
-intros p Hrec b.
+intros p Hrec _ b.
 generalize (Z_div_mod b (Zpos p)).
 case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
 elim Hqr; clear Hqr; intros; auto with zarith.
@@ -405,8 +405,7 @@ split; auto.
 rewrite H.
 apply Zis_gcd_for_euclid2; auto.
 
-intros p Hrec b.
-exists 0; intros.
+intros p _ H b.
 elim H; auto.
 Defined.