diff options
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Ed25519.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 5107c1468..fa1c44d08 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -359,7 +359,7 @@ Proof. reflexivity. } Unfocus. - cbv iota beta delta [point_dec_coordinates ModularWordEncodingTheorems.sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. etransitivity. Focus 2. { |