diff options
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index c527ea279..2a0978192 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -30,6 +30,10 @@ Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Util.Notations. Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Hints.PullPush. Import ListNotations. Local Open Scope Z_scope. Module Associational. @@ -617,10 +621,6 @@ Module BaseConversion. End BaseConversion. End BaseConversion. -Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Hints.PullPush. - Module Saturated. Section Weight. Context (weight : nat->Z) |