diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-03-09 10:15:02 +0100 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2018-04-03 09:00:55 -0400 |
| commit | 1d9f510e4e99469dc78f50d116be198677c1cf7f (patch) | |
| tree | 9c1cae14bb9ecca21c7dc238fa20674420d70990 | |
| parent | 209242534fa7c991d748079c5af5b182b38342ac (diff) | |
move requires to the top of the file
| -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) |