diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 2 |
4 files changed, 10 insertions, 10 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index c115a831d..04fc5a8df 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -369,7 +369,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H; clear H; intros. + destruct 1; injection H as ? ?. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -411,7 +411,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1; clear H1; intros. + injection H1 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -522,7 +522,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4; clear H4; intros. + injection H4 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 56cb9bbc2..7c76011f2 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -138,7 +138,7 @@ intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 8673b8a58..63fb5800c 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -427,13 +427,13 @@ Module Make (NN:NType) <: ZType. (* Pos Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos py) with (Zneg py). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -442,13 +442,13 @@ Module Make (NN:NType) <: ZType. (* Neg Pos *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos px) with (Zneg px). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -457,7 +457,7 @@ Module Make (NN:NType) <: ZType. (* Neg Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto). + try (injection 1 as -> ->; auto). simpl. intros <-; auto. Qed. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index ec1017f50..e8ff516f3 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -110,7 +110,7 @@ intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. |