aboutsummaryrefslogtreecommitdiff
path: root/src/Util/WordUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/WordUtil.v')
-rw-r--r--src/Util/WordUtil.v5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 2faafe6c6..932f48fee 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -9,12 +9,15 @@ Require Import Coq.Bool.Bool.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.RewriteHyp.
Require Import Crypto.Util.Sigma.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.N2Z.
+Require Import Crypto.Util.ZUtil.Definitions.
+
Require Import bbv.WordScope.
Require Import bbv.Nomega.