diff options
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Ed25519.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index b9d6cf134..f02c24ffb 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -5,7 +5,8 @@ Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. Require Import ModularArithmetic.ModularArithmeticTheorems. Require Import ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. +Require Import Crypto.Encoding.PointEncodingPre. +Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.PointEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Util.IterAssocOp. @@ -469,8 +470,6 @@ Proof. set_evars. rewrite !FRepOpp_correct. - rewrite <-!enc_rep2F_correct. - rewrite <-wltu_correct. rewrite (if_map rep2F). lazymatch goal with |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) => |