diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-03 23:53:11 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-03 23:53:11 -0500 |
| commit | a78706d510db71e8555c22ce8989814b28934e51 (patch) | |
| tree | 880fc218a055d487f13bfc5471b3221b3048c929 /src/Experiments | |
| parent | 23f642ce06af7f9141b406f5a1d23f9f62a34097 (diff) | |
Fix changed names
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 59756c0a1..b93272a3d 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -1137,8 +1137,8 @@ Lemma pow2_mod_range : forall a n m, Proof. intros; unfold ZUtil.Z.pow2_mod. rewrite Z.land_ones; [|assumption]. - split; [apply Z.mod_pos_bound, WordUtil.Z_pow2_gt_0; assumption|]. - eapply Z.lt_le_trans; [apply Z.mod_pos_bound, WordUtil.Z_pow2_gt_0; assumption|]. + split; [apply Z.mod_pos_bound, ZUtil.Z.pow2_gt_0; assumption|]. + eapply Z.lt_le_trans; [apply Z.mod_pos_bound, ZUtil.Z.pow2_gt_0; assumption|]. apply Z.pow_le_mono; [|assumption]. split; simpl; omega. Qed. @@ -1153,7 +1153,7 @@ Proof. intros a n m H0 H1 H2; destruct H2. split; [apply Z.shiftr_nonneg; assumption|]. rewrite Z.shiftr_div_pow2; [|assumption]. - apply Z.div_lt_upper_bound; [apply WordUtil.Z_pow2_gt_0; assumption|]. + apply Z.div_lt_upper_bound; [apply ZUtil.Z.pow2_gt_0; assumption|]. eapply Z.lt_le_trans; [eassumption|apply Z.eq_le_incl]. apply Z.pow_add_r; omega. Qed. |