diff options
Diffstat (limited to 'src/Arithmetic/BarrettReduction/RidiculousFish.v')
-rw-r--r-- | src/Arithmetic/BarrettReduction/RidiculousFish.v | 2 |
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. |