diff options
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v | 2 | ||||
| -rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Core.v | 1 | ||||
| -rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Montgomery.v | 1 |
3 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v index 7274d2c35..58f5279ab 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v @@ -6,7 +6,7 @@ Require Import Crypto.Arithmetic.Core. Import B. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. +Require Import Crypto.Util.LetIn. Require Import Crypto.Arithmetic.Karatsuba. Require Import Crypto.Util.Tactics.BreakMatch. Require Crypto.Util.Tuple. diff --git a/src/Specific/NISTP256/FancyMachine256/Core.v b/src/Specific/NISTP256/FancyMachine256/Core.v index fec353c6f..881fa2e1e 100644 --- a/src/Specific/NISTP256/FancyMachine256/Core.v +++ b/src/Specific/NISTP256/FancyMachine256/Core.v @@ -20,7 +20,6 @@ Require Import Crypto.Compilers.Linearize. Require Import Crypto.Compilers.Inline. Require Import Crypto.Compilers.CommonSubexpressionElimination. Require Export Crypto.Compilers.Reify. -Require Export Crypto.Util.ZUtil. Require Export Crypto.Util.Option. Require Export Crypto.Util.Notations. Require Import Crypto.Util.ListUtil. diff --git a/src/Specific/NISTP256/FancyMachine256/Montgomery.v b/src/Specific/NISTP256/FancyMachine256/Montgomery.v index b8510614e..4caecca6b 100644 --- a/src/Specific/NISTP256/FancyMachine256/Montgomery.v +++ b/src/Specific/NISTP256/FancyMachine256/Montgomery.v @@ -1,6 +1,7 @@ Require Import Crypto.Specific.NISTP256.FancyMachine256.Core. Require Import Crypto.LegacyArithmetic.MontgomeryReduction. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. +Require Import Crypto.Util.ZUtil.EquivModulo. Section expression. Context (ops : fancy_machine.instructions (2 * 128)) (props : fancy_machine.arithmetic ops) (modulus : Z) (m' : Z) (Hm : modulus <> 0) (H : 0 <= modulus < 2^256) (Hm' : 0 <= m' < 2^256). |