diff options
Diffstat (limited to 'src/LegacyArithmetic/ZBoundedZ.v')
| -rw-r--r-- | src/LegacyArithmetic/ZBoundedZ.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/LegacyArithmetic/ZBoundedZ.v b/src/LegacyArithmetic/ZBoundedZ.v index fef654f47..2943598c1 100644 --- a/src/LegacyArithmetic/ZBoundedZ.v +++ b/src/LegacyArithmetic/ZBoundedZ.v @@ -1,7 +1,9 @@ (*** ℤ can be a bounded ℤ-Like type *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Pow2Mod. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. |