diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
| commit | cc920cf2a3aa859a93e8e990a19a960f78cd3b1b (patch) | |
| tree | ed93d93f82578239ef2e0a6843e52e1d6968a5ef /src/ModularArithmetic/Pow2BaseProofs.v | |
| parent | 260b20cab885deae59a305492567dc0f0d88b3a8 (diff) | |
| parent | 0cea3e2f80408a25954f820faebf5cd79d2e13ae (diff) | |
Merged changes, including new ZUtil conventions.
Diffstat (limited to 'src/ModularArithmetic/Pow2BaseProofs.v')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 23393d7ef..1504ca0df 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -97,7 +97,7 @@ Section Pow2BaseProofs. Proof. intros. repeat rewrite nth_default_base by omega. - apply mod_same_pow. + apply Z.mod_same_pow. split; [apply sum_firstn_limb_widths_nonneg | ]. destruct (NPeano.Nat.eq_dec i 0); subst. + case_eq limb_widths; intro; unfold sum_firstn; simpl; try omega; intros l' lw_eq. @@ -199,7 +199,7 @@ Section BitwiseDecodeEncode. intros. simpl; f_equal. match goal with H : bounded _ _ |- _ => - rewrite Z_lor_shiftl by (auto; unfold bounded in H; specialize (H i); assumption) end. + rewrite Z.lor_shiftl by (auto; unfold bounded in H; specialize (H i); assumption) end. rewrite Z.shiftl_mul_pow2 by auto. ring. Qed. |