aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/ArithmeticSimplifierWf.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Z/ArithmeticSimplifierWf.v')
-rw-r--r--src/Compilers/Z/ArithmeticSimplifierWf.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index ff690688a..4efa7445a 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -10,7 +10,6 @@ Require Import Crypto.Compilers.Z.OpInversion.
Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
Require Import Crypto.Compilers.Z.Syntax.Equality.
Require Import Crypto.Compilers.Z.Syntax.Util.
-Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Sum.
Require Import Crypto.Util.Prod.