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.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 68f477505..4833f0df6 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -10,7 +10,9 @@ 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.
+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 Bedrock.Word.