diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-12 11:56:06 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-12 11:56:06 -0400 |
| commit | e8f3cdec7613d26d4cd15bf2fb80e8576d4f2d62 (patch) | |
| tree | bf291839b3570c35eeead471b21379481fc3e6c8 /src | |
| parent | 8a6069788d24878f0a4735c72e0116fba34c968c (diff) | |
Fixed syntax error (missing bracket) in Ed25519 to make merge build
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/Ed25519.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index fbcedae47..6e4bea1e5 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -344,11 +344,12 @@ Proof. rewrite (rep2F_F2rep Ed25519.d), (rep2F_F2rep Ed25519.a), (rep2F_F2rep 1%F). rewrite !FRepMul_correct. rewrite !FRepSub_correct. + cbv zeta. rewrite F_pow_2_r. cbv beta delta [twistedToExtended]. cbv beta iota delta [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd - point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q + point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q ]. Admitted. |