From 76adb57c72fccb4f3e416bd7f3927f4fff72178b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 1 Jun 2014 10:26:26 +0200 Subject: Making those proofs which depend on names generated for the arguments in Prop of constructors of inductive types independent of these names. Incidentally upgraded/simplified a couple of proofs, mainly in Reals. This prepares to the next commit about using names based on H for such hypotheses in Prop. --- theories/ZArith/Zdigits.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/ZArith') diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 8a9497682..e5325aa75 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -216,10 +216,10 @@ Section Z_BRIC_A_BRAC. omega. rewrite <- two_power_nat_S. - destruct (Zeven.Zeven_odd_dec z); intros. + destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros. rewrite <- Zeven.Zeven_div2; auto. - generalize (Zeven.Zodd_div2 z z0); omega. + generalize (Zeven.Zodd_div2 z Hodd); omega. Qed. Lemma Z_to_two_compl_Sn_z : -- cgit v1.2.3