Factor out some bedrock dependencies into WordUtil

Also move a definition about words, with a TODO about location, into WordUtil.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index adc40dae6..e16cc73f6 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -4,7 +4,7 @@ Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding.
 Require Import Crypto.Spec.EdDSA.
 Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil.
+Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil.
 Require Import Bedrock.Word.
 Require Import VerdiTactics.
 Require Import Decidable.
@@ -150,7 +150,7 @@ Instance x : EdDSAParams := {
   FqEncoding := FqEncoding;
   FlEncoding := FlEncoding;
   PointEncoding := PointEncoding;
- 
+
   b_valid := b_valid;
   c_valid := c_valid;
   n_ge_c := n_ge_c;