aboutsummaryrefslogtreecommitdiff
path: root/src/PushButtonSynthesis/BarrettReduction.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/PushButtonSynthesis/BarrettReduction.v')
-rw-r--r--src/PushButtonSynthesis/BarrettReduction.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v
index 504a26a0c..19014ffec 100644
--- a/src/PushButtonSynthesis/BarrettReduction.v
+++ b/src/PushButtonSynthesis/BarrettReduction.v
@@ -10,7 +10,7 @@ Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Language.
Require Import Crypto.CStringification.
-Require Import Crypto.Arithmetic.
+Require Import Crypto.Arithmetic.BarrettReduction.
Require Import Crypto.BoundsPipeline.
Require Import Crypto.Fancy.Compiler.
Require Import Crypto.COperationSpecifications.