diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-04-11 17:55:43 +0200 |
|---|---|---|
| committer | Jade Philipoom <jadep@google.com> | 2018-04-11 17:55:43 +0200 |
| commit | 50a2831e9456de1a82456ca6fde648d389cca941 (patch) | |
| tree | 578718ad913d3e4ad78590858d000a81a3ce40b6 /src | |
| parent | 5bcaffd6bcb26d1643484e2551e10cfbd78f2d22 (diff) | |
move requires to top of file
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 4f4eb5683..3845c8781 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -12,6 +12,9 @@ Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. Require Import Crypto.Algebra.Ring. Require Import Crypto.Algebra.SubsetoidRing. Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Arithmetic.BarrettReduction.Generalized. +Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. +Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. @@ -31,10 +34,13 @@ 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.CC Crypto.Util.ZUtil.Rshi. +Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. 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. +Require Import Crypto.Util.ZUtil.EquivModulo. Import ListNotations. Local Open Scope Z_scope. Module Associational. @@ -7748,10 +7754,6 @@ End X25519_32. *) -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. - Module BarrettReduction. (* TODO : generalize to multi-word and operate on (list Z) instead of T; maybe stop taking ops as context variables *) Section Generic. @@ -8210,12 +8212,6 @@ Module BarrettReduction. End BarrettReduction. End BarrettReduction. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Tactics. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. - Module MontgomeryReduction. Section MontRed'. Context (N R N' R' : Z). |