diff options
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 7ece3a5da..b0323c4a0 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -11,6 +11,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. @@ -33,8 +34,7 @@ Definition mul2modulus : fe25519 := Instance subCoeff : SubtractionCoefficient modulus params25519. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - apply ZToField_eqmod. - cbv; reflexivity. + vm_decide. Defined. Definition freezePreconditions25519 : freezePreconditions params25519 int_width. |