diff options
Diffstat (limited to 'src/Specific/NISTP256')
-rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Core.v | 1 | ||||
-rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Montgomery.v | 1 |
2 files changed, 1 insertions, 1 deletions
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). |