From e1e0f4f7f3c549fd3d5677b67c6b13ed687e6f12 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 3 Jun 2014 17:15:40 +0200 Subject: Make standard library independent of the names generated by induction/elim over a dependent elimination principle for Prop arguments. --- theories/ZArith/Znumtheory.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/ZArith') diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 594c07356..c741f4bc4 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -308,11 +308,11 @@ Section extended_euclid_algorithm. intros v3 Hv3; generalize Hv3; pattern v3. apply Zlt_0_rec. clear v3 Hv3; intros. - elim (Z_zerop x); intro. + destruct (Z_zerop x) as [Heq|Hneq]. apply Euclid_intro with (u := u1) (v := u2) (d := u3). assumption. apply H3. - rewrite a0; auto with zarith. + rewrite Heq; auto with zarith. set (q := u3 / x) in *. assert (Hq : 0 <= u3 - q * x < x). replace (u3 - q * x) with (u3 mod x). -- cgit v1.2.3