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