aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/BarrettReduction/RidiculousFish.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Arithmetic/BarrettReduction/RidiculousFish.v')
-rw-r--r--src/Arithmetic/BarrettReduction/RidiculousFish.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/BarrettReduction/RidiculousFish.v b/src/Arithmetic/BarrettReduction/RidiculousFish.v
index b9697839d..af030dcfe 100644
--- a/src/Arithmetic/BarrettReduction/RidiculousFish.v
+++ b/src/Arithmetic/BarrettReduction/RidiculousFish.v
@@ -1,5 +1,5 @@
Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Hints.ZArith.
Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.