aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/BarrettReduction/ZHandbook.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/ModularArithmetic/BarrettReduction/ZHandbook.v')
-rw-r--r--src/ModularArithmetic/BarrettReduction/ZHandbook.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/BarrettReduction/ZHandbook.v b/src/ModularArithmetic/BarrettReduction/ZHandbook.v
index 3fc1214eb..b0d6480d8 100644
--- a/src/ModularArithmetic/BarrettReduction/ZHandbook.v
+++ b/src/ModularArithmetic/BarrettReduction/ZHandbook.v
@@ -9,7 +9,7 @@
have to carry around extra precision), but requires more stringint
conditions on the base ([b]), exponent ([k]), and the [offset]. *)
Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.Tactics Crypto.Algebra.
+Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch Crypto.Algebra.
Local Open Scope Z_scope.