From 1d9f510e4e99469dc78f50d116be198677c1cf7f Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Fri, 9 Mar 2018 10:15:02 +0100 Subject: move requires to the top of the file --- src/Experiments/SimplyTypedArithmetic.v | 8 ++++---- 1 file 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) -- cgit v1.2.3