aboutsummaryrefslogtreecommitdiff
path: root/src/LegacyArithmetic/BaseSystemProofs.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/LegacyArithmetic/BaseSystemProofs.v')
-rw-r--r--src/LegacyArithmetic/BaseSystemProofs.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v
index f0f0a80d2..042fdb270 100644
--- a/src/LegacyArithmetic/BaseSystemProofs.v
+++ b/src/LegacyArithmetic/BaseSystemProofs.v
@@ -1,5 +1,5 @@
Require Import Coq.Lists.List Coq.micromega.Psatz.
-Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.ListUtil.
Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
Require Import Crypto.LegacyArithmetic.BaseSystem.